Why a Formally Checked Proof May Not Prove What You Meant
A proof can compile and check while proving the wrong statement. The three-gate model shows what a formalization must clear before it is trusted.
Yash Sharma5 min readEvaluation and assurance
Research area 82: Autonomous mathematical formalization and statement-faithfulness engineering
In brief
- A formal proof that compiles and checks can still prove the wrong statement.
- The three-gate model requires a claim to compile, stay faithful, and be checked.
- The value is avoided false certification, not a productivity number.
Autonomous mathematical formalization and statement-faithfulness engineering is the discipline of making sure an AI system that turns a mathematical claim into a machine-checked proof has actually proved that claim, not a different one that merely compiles. A proof checker confirms a formal statement follows from stated axioms. It cannot confirm the statement is the theorem anyone meant, and that gap matters the moment a verified result is cited as settled.
What it is
Three events must occur before a formalization result is worth trusting, and treating any one as proof of the others is the field's most common mistake. The claim must compile: the toolchain accepts the statement as well formed. It must be faithful: the statement matches the quantifiers, domains, definitions, and side conditions of the claim someone meant. And it must be proven: a trusted checker accepts a complete proof against an audited set of axioms, with no unresolved placeholders. I call this the three-gate model, because the three events fail independently and a result counts only once it clears all three.
Compiling and being faithful are not the same claim. Swapping the order of two quantifiers, or reusing an expression under a different number type, produces a statement that compiles cleanly while proving something else entirely.
Novelty is a separate question above all three gates: formalizing an existing theorem and proving something genuinely new need different evidence and should never be priced the same. The trusted base, the checker's kernel, its axioms, and every imported library, must be audited as one unit, since search cannot enlarge what is valid unless the base or the statement changes. Reuse of prior libraries and earlier human work must be tracked and disclosed.
Why it matters now
The stakes changed in September 2026, when a formalization of Fermat's Last Theorem was released with a pinned proof artifact and a verification contract. The project reportedly ran about eleven days and consumed roughly six billion output tokens from an internal model working with a tool called Prove2Me, building on substantial prior human formal mathematics. That is formalization of an existing theorem, not new mathematics, and the announcement alone is a first-party claim whose autonomy and cost have not been independently normalized. Kevin Buzzard of the Xena Project then compiled the released project himself and ran its verification comparator, confirming the argument and finding reused small-prime formalizations inside it, a materially stronger assurance than the announcement alone.
The failure mode is not hypothetical. A benchmark that perturbed 12,784 reasoning steps across eight formalization systems found that formal statements can silently correct an invalid step, collapse a domain, or accept a vacuous claim while passing every compilation check.
The architecture
The three-gate model is a flow, not a checklist, and each gate has its own owner. Work starts with statement extraction: the informal claim's terms are pulled out and reviewed by a mathematician independent of whoever will search for the proof. That reviewed target is then frozen, and any later change to it is a specification revision that must go back through the same review.
Proof construction comes next and is the noisiest part by design: retrieval proposes lemmas, tactics explore transformations, decomposition invents intermediate lemmas, and none of it counts until the checker validates the result against the frozen statement and the audited trusted base.
Each gate fails differently. Gate one fails loudly, since the toolchain simply rejects the statement. Gate two fails silently, which makes it dangerous: a dropped positivity condition or a reordered quantifier compiles without complaint while quietly changing the claim. Gate three fails through the trusted base, where an unaudited placeholder can let a checked-looking result through unreviewed. Independent statement review closes gate two, a clean rebuild with a full axiom audit closes gate three, and neither substitutes for the other.
How to lead it
One senior technical leader owns this, separate from whoever owns the proof-search system, since self-certification is not an acceptance track. Fund review capacity before a faster search system, since a backlog there is where faithfulness failures accumulate unseen. Measure the rate results clear all three gates, not the rate they compile, and disclose failed attempts rather than only the final theorem count.
Stop treating a compiling statement as proof of the claim, stop pricing an internal model's cost against an unrelated public API rate, and stop announcing a result as settled before independent corroboration exists. Three decisions stay with the executive alone: whether an unaudited external solver may sit inside the trusted base, how much residual risk to carry given the lack of evidence for general competence on unfamiliar mathematics, and when a novel-theorem claim needs outside review before anyone relies on it.
What it is worth
The value here is avoided false certification, not a productivity number, and the evidence does not support inventing one. A formally checked proof of the wrong statement is a confidently wrong answer with a mathematical seal on it, and the cost of that seal being trusted downstream can dwarf the cost of the review that would have caught it. What the evidence supports is narrower than an announcement suggests: the outside verification of the September 2026 artifact establishes that a specific released result checks out in a specific environment, not general competence on unfamiliar mathematics. Cost accounting is incomplete for the same reason: search tokens, failed attempts, checking, and human time should be counted separately, and any internal model cost that cannot be measured directly should be reported as unknown rather than estimated from an unrelated price.
Questions leaders ask
- Does a formal proof that compiles and checks mean the underlying claim is actually true?
- No. Compiling only means the toolchain accepted the statement as well formed. A statement can compile cleanly while swapping a quantifier order, dropping a side condition, or reusing an expression under the wrong number type, all of which change the claim entirely. Only a claim that compiles, is independently reviewed as faithful, and is then checked against an audited trusted base has been proven.
- What did the September 2026 Fermat's Last Theorem formalization actually achieve?
- It formalized an existing, already proven theorem using substantial prior human formal mathematics, not a discovery of new mathematics. The project reportedly ran roughly eleven days and used about six billion output tokens from an internal model alongside a tool called Prove2Me. Kevin Buzzard of the Xena Project independently compiled the released artifact and ran its verification check, a materially stronger form of assurance than the announcement alone.
- Can a model's own confidence that its formal statement matches the informal one be trusted?
- No. A benchmark that perturbed 12,784 reasoning steps across eight formalization systems found that formal statements can silently correct an invalid step, collapse a domain, or accept a vacuous claim while still passing every compilation check. Faithfulness needs independent back-translation, counterexample search, and expert review, and even those checks are not a complete guarantee of meaning.
- Is successfully rebuilding a proof project in a clean environment enough to accept its result?
- It establishes that the exact reported artifact is derivable inside that specific pinned environment, which is valuable and often skipped. It does not establish that the informal statement was faithfully translated or that the trusted base matches the declared foundation. A clean rebuild has to be paired with an independent statement review and a full axiom audit, not treated as a substitute for either.
- How should an organization measure the real cost of an autonomous formalization project?
- Count search tokens, failed attempts, proof checking, infrastructure, and human interventions separately, and record elapsed time alongside them. Report any internal model cost that cannot be directly measured as unknown, rather than estimating it by multiplying token counts against an unrelated public API price. A single large successful project also does not establish the cost of the next one on different mathematics.
