Accountability

The Declaration asksTransparently report automated tools, including LLMs and proof assistants, in a form consistent with open-science norms.

Disclosure is structural, not sectional. Every public claim carries an epistemic grade (Proved / Measured / Model / Play) with a public legend. The authorship model is stated plainly: AI systems are primary authors of proofs and code; a human orchestrator directs the work and bears full responsibility. Disclosure is also per-artifact — blog posts name the specific model that wrote them, because conflating several models under one byline would be less honest than naming who wrote what. The toolchain identity is itself a locked, gated artifact: the tools are not merely named, they are pinned, and their versions are part of every claim's provenance.

• Epistemic grading legend
• Authorship model and non-claims
• Toolchain lock (pinned, gated)

Row verified 2026-07-30

The Declaration asksMake reviewing feasible — disclose tools, give precise references, provide formal proofs where appropriate.

The artifacts are formal by construction. Headline theorems ship with machine-checkable axiom footprints that a reviewer can re-derive with one command, rather than trusting our summary of what a proof assumes. The evidence is published, not just the tool: our eighteen-version toolchain migration measured footprint equality against a frozen v4.14.0 baseline — never chained through an intermediate, because chaining would let a drift launder itself across two comparisons — and the snapshots, per-stop verdicts and hashed baselines are all readable.

• Migration log (v4.14.0 → v4.32.2, with its own corrections)
• Frozen v4.14.0 baseline footprints
• Destination verdict (v4.32.2)
• footprint_snapshot.py (the re-derivation tool)
• Axiom ledger

Row verified 2026-07-30

The Declaration asksTransparency and accessibility of research, data, and software.

Repositories are public, the package is on PyPI, the preprint is on arXiv, and the reproduction zoo serves its whole evidence tree as static assets — the evidence is the website. What is not yet open is stated in the peer-review row rather than hidden here.

• Source (GitHub)
• Package (PyPI)
• Preprint (arXiv:2603.21852)
• Reproduction zoo

Row verified 2026-07-30

The Declaration asksWhen automated techniques are used, responsibility for correctness remains exclusively with the human authors.

Accepted — and mechanized, because a pledge is not a mechanism. Correctness is discharged through sorry audits (a count that cannot be derived is treated as an instrument failure, not a zero), an axiom ledger gated in CI in both directions, kernel replay through an external checker, and acceptance bars fixed before the data exists. The failures stay in the record rather than being amended away: the migration log carries a correction stating that a stop was committed as “accepted” before its central criterion had ever been measured, and the amendment trail records a pass bar being weakened in the open, with the byte-identical check that proved the weakening changed nothing else.

• Pass bar and Amendments 1–5
• Migration log, including its own corrections
• checkpoint.py (the pass bar, executable)
• Axiom ledger

Row verified 2026-07-30

The Declaration asksCredit and responsibility belong to humans; AI does not replace the collective human labor behind a result.

No AI system is listed as an author of any Monogate publication or claim. The orchestrator model is stated in plain terms: the human directs, selects, and answers for everything; the AI's role is disclosed but carries neither credit nor responsibility. We also state the corollary the Declaration is careful about — our results synthesize decades of human work (Lean and its community, the numerics-verification lineage, classical estimation theory), and our novelty claims are scoped accordingly: composition and discipline, not new mathematics.

• Authorship model, division of labor, explicit non-claims
• Preprint (prior art and lineage)

Row verified 2026-07-30

The Declaration asksProactive effort to find and credit sources; where satisfactory attribution is not possible, state this explicitly.

We cite the human lineage we know and can trace, in the paper and in per-file references across the repositories, and we review prior art before making a novelty claim.

The named gapThe AI systems we use are trained on corpora whose provenance we cannot audit or certify. Their outputs may synthesize uncredited human work in ways invisible to us. Per the Declaration's own provision we state this explicitly rather than launder it: attribution through the model is not attribution, and we cannot certify it.

What would change the gradeGrade moves to MET when an attribution section audited against the final paper's related-work review ships with a peer-reviewed version. The training-corpus gap is not closable by us and will remain stated.

• Preprint (arXiv:2603.21852)
• Authorship and lineage statement

Row verified 2026-07-30

The Declaration asksEngage publicly to explain and contextualize AI-assisted methods and results, including support for science journalism.

This page, the incident report below it, the public grading legend, and interactive explanations of the mathematics aimed at non-specialists.

The named gapNo engagement yet with science journalism or community venues where these claims would be examined by people with no reason to be kind. Public artifacts are necessary but not sufficient for discourse: publishing is not the same as being questioned.

What would change the gradeGrade moves to MET when the work has been presented and questioned in at least one community venue — a talk, a workshop, or peer commentary on a published paper.

• This page
• Incident report: July 2026 Lean kernel bug
• Interactive explanations

Row verified 2026-07-30

The Declaration asksStay informed about the capabilities of computer-aided tools as appropriate to one's research.

Standing watches with recorded reference states, not impressions: a quarterly watch re-scans the external verification ecosystem and reports movement against recorded state, upstream issue threads are tracked as part of it, and the July 2026 Lean kernel soundness disclosure was triaged and acted on in the week it landed. When we found the independent checker broken at every version we could use, we reported it upstream with minimal reproductions rather than routing around it.

• Expiry watch (tool)
• Watch state (recorded reference point)
• Upstream report we filed (lean4lean #17)
• Incident report

Row verified 2026-07-30

The Declaration asksMake standards and practices explicit and accessible; create pathways for participation.

The standards are unusually explicit and public — a grading legend, a schema for submitted records, and a contributor guide covering what we accept, how to format a record, and how it is verified. Failure data is explicitly welcome as a contribution, which is unusual and deliberate.

The named gapThe pathway that exists is for submitting new proof records. There is no pathway for the thing this page is really about — independently reproducing an acceptance from raw artifacts — and no external contributor has yet done so. The documentation is a working record, not an on-ramp for a reviewer.

What would change the gradeGrade moves to MET when at least one external reproduction of a zoo card's acceptance from raw artifacts is on record, and a reproduction guide exists alongside the contribution guide.

• Contributor guide
• Record schema
• Reproduction zoo (intended first pathway)

Row verified 2026-07-30

The Declaration asksWeigh alignment, openness, energy, and scale when choosing tools — including whether to use AI at all.

Tool choices are recorded decisions with stated trade-offs, including a decision to sit on an unpatched-but-dual-checkable kernel version until the external-checker intersection moved — and the later reversal of that decision when its premise was refuted by primary sources. The verification substrate is deliberately open and small: a Mathlib-free library with an audited axiom base, chosen so that trust reduces to a readable core.

The named gapThe AI authorship itself runs on large commercial models whose training practices, energy costs, and corporate policies we do not control and cannot audit. Using them is a considered choice — this project exists to test what discipline can be maintained around exactly these tools — and this row exists so that the choice is on the record as a choice rather than a default.

What would change the gradeNo upgrade path is claimed while the models we depend on remain unauditable. This row is expected to stay PARTIAL.

• Recorded decisions and their reversals (Amendments 1–5)
• Axiom ledger (the readable core)

Row verified 2026-07-30

The Declaration asksResults must be published in peer-reviewed venues; informal channels support but cannot replace community scrutiny.

A preprint exists. The zoo, 1op.io, and this site are informal channels in exactly the Declaration's sense — every claim on them links to regenerable artifacts, which mitigates but does not substitute for peer review. A paper targeting a formal-methods venue is in preparation.

The named gapUntil that paper is submitted, reviewed, and published, the Declaration's fourth threat — that proper evaluation is endangered when results are communicated through informal channels, often without any research paper — applies to this project. This row exists to say so rather than to let the artifact links imply that the question is settled.

What would change the gradeGrade moves to PARTIAL when the paper is under submission, and to MET when it is published.

• Preprint (arXiv:2603.21852)

Row verified 2026-07-30

The Declaration asksEvaluate ethical consequences; withdraw from harmful work; partner only where values are respected.

Stated plainly rather than abstractly: our application domain is safety-critical estimation and control, and the worked examples are Kalman-class filters including range-bearing tracking — a technology class with civilian uses (navigation, robotics, medical devices, automotive safety) and defense-relevant ones. Our position: the contribution is evidence discipline, making safety-critical systems provably match their specifications, and we hold that verified correctness in deployed systems is a public good. We have no defense contracts; any future partnership will be evaluated against this row and recorded on this page.

The named gapWe do not claim this settles the ethics. We claim it is disclosed, and that the disclosure has a maintenance rule. Ethical evaluation is not a completable task.

What would change the gradeNone. This row is graded PARTIAL permanently by design — a MET here would overclaim.

• This row (disclosure of record)

Row verified 2026-07-30

The Declaration asksInstitutional and policy recommendations — publication norms, funding, evaluation infrastructure, and community standards.

Noted for completeness. These recommendations address institutions rather than individual researchers. Where one lands on us in practice — the obligation to publish through peer-reviewed venues — it appears above as its own row rather than being filed here where it would be easy to ignore.

• Leiden Declaration (full text)

Row verified 2026-07-30