10. Autoformalization and statement fidelity

The kernel answers one question perfectly: is this Lean term a proof of this Lean type? It cannot answer the question that matters: does this Lean type say what the mathematician meant? That second question is fidelity. In 2026 it is the weakest link in all formal mathematics, with AI or without it. This document tells how to change fidelity from a hope into a property that we measure, review and maintain.

10.1 The evidence that this is the bottleneck

Document 01 has the sources. In brief:

• An audit in 2025 found that about a third of the Lean 4 port of ProofNet was misformalized.
• An ICML 2026 audit of five formal benchmarks found 4,833 issues. Of these, 398 were mechanically certified: counterexamples to stated theorems, vacuous statements, and unsound axioms.
• The statements of PutnamBench needed 27 fixes from one prover team and 2 more from another before people could call the benchmark saturated.
• In 2025, an AI "solution" to an Erdős problem got much attention. It proved a weaker variant, because the problem as written did not have a hypothesis.
• The 2026 Navier–Stokes claim came with a Lean proof. The dispute about it was about the gap between the formal statement and the physical problem.
• The 2026 Annals Challenge put Lean statements of 50 recent Annals theorems into Mathlib. It found that the main blocker was missing definitions, not missing proofs.
• In the largest 2026 formalizations, people fixed or cross-checked the top-level statement by hand, against a curated library. In the Fermat run, agents cross-checked the intermediate statements of each other, and that found false ones early.

The lesson that math2 takes: autoformalization of statements is now cheap and usually right. "Usually" is not good enough for a library that other work will build on. Thus the pipeline has two halves. A cheap machine half, F1, finds most errors. A human half, F2 and F3, is made fast enough that people can review the important statements.

10.2 The formalize pipeline

The formalize role (12.1) runs this pipeline for one node. m2 autoform <tag> runs it from the command line.

1. context      node statement, its uses closure (definitions!), sources' locators,
                bound neighbours and their Lean statements, Mathlib conventions
2. definitions  every concept the statement uses must already be bound, or is formalized first (10.3)
3. candidates   k candidate Lean statements from ≥ 2 model families, each elaborated in a Lean session
4. battery      the F1 battery (10.4) on every candidate that elaborates
5. select       candidates that pass; clustered by type hash and by proved equivalence;
                the largest agreeing cluster wins; disagreement is itself recorded
6. propose      PR: binding at F0 with the winning statement, the battery report,
                the dissenting candidates, and a review packet (10.6)

Two design points:

• Agreement among independent candidates is evidence. Five candidates from two model families can elaborate to the same type hash, or to types proved equivalent in a Lean session. That is stronger than the back-translation of one candidate. If the candidates split into clusters, the split usually points directly at the ambiguity: which convention for $\mathbb{N}$, whether "ring" includes a unit, whether a sum is over a finite set. The PR reports it.
• Search before writing. Step 1 first searches for an existing declaration with type search (14.3) and embedding search. If Mathlib already states it, the binding goes to Mathlib, and the formalize run becomes an align run.

10.3 Definitions before statements

A statement can only be as faithful as the definitions that it uses. A faithful statement about the wrong notion of "regular" is wrong. Thus formalize works from the bottom up over the uses closure:

1. Each concept or definition node in the closure must have a binding at F2 or higher before a statement that uses it can go higher than F1. The fidelity queue enforces this review order (11.4 unlock).
2. If Mathlib has no definition, the formalize role proposes one in Math2/, together with sanity lemmas. These show that the definition agrees with the examples of the textbook and with known equivalent characterisations. The proof of the sanity lemmas is a prove job. A definition with proved sanity lemmas is much easier to review.
3. If Mathlib has several candidate definitions (bundled and unbundled, Set and Finset, different universe levels), the binding names the selected one, and the remarks of the node say why.

10.4 The F1 battery

F1 means that a candidate has passed each check that needs no human. A candidate is a statement: a theorem, or a definition of a proposition when the result has no proof yet (07.2). The battery report records each check. Each check has an evaluation set with a measured detection rate (17.3).

A candidate is F1 if checks 1, 3, 4, 6, 7, 8 and 10 pass, and checks 2 and 9 raise no high-severity concern. Check 5 never blocks F1. Sometimes a trivial truth is the correct statement. But the review packet always shows a trivial truth.

Checks 4, 5 and 6 are also rule F09. This rule runs on each F1+ binding at each release, because a Mathlib bump can make a statement trivial or vacuous and not change its text.

The battery in m2. The package battery runs the checks. The build step battery runs after the replay step and writes build/battery.json, with one report for each Lean binding. The status step reads the reports and gives F1 to a binding when its report is F1. Each check gives one of six results: pass, fail, flag, open, skip or not-run. A blocking check passes F1 with pass, flag or skip. Checks 2 and 9 pass F1 with pass or flag. Thus an open or not-run result blocks F1. The checks work as follows:

• Check 1 uses the extraction record of the declaration.
• Check 3 maps each constant of the statement to the nodes that bind it. The constants of logic and notation, and the instances, do not need a node. A constant that no node binds gives open. A set of patterns on the pp.all statement finds the junk values of 10.5 (natural subtraction, division by zero, Real.sqrt, Real.log and others) and gives a flag with the class M-junk.
• Checks 4, 5 and 6 use the degenerate-statement checks of the extract step.
• Checks 7 and 8 ask a Lean session for a short tactic proof of A → B or of A → ¬B, with the implies command of M2Extract. Check 7 does not instantiate the statement yet. It compares the statement with the formal statement of each example and counterexample of its concepts. When the statement implies the negation of an example, the class is M-strong. When a counterexample implies the negation of the statement, the class is M-hyp-missing. Check 8 uses the edges generalizes, specializes, implies and equivalent.
• Check 10 uses the comparator result of the replay step.
• Checks 2 and 9 need models. The build does not run them until the model calls are approved, so no binding is F1 before then.

10.5 A taxonomy of misformalization

Each class has a name, a detector and an example. Reviews and audit samples get labels from these classes. Thus we can measure the error rate for each class (17.3), and we can improve the battery where it is weak.

10.6 Human review: F2 and F3

What a reviewer signs

A fidelity review says: I have read the informal statement with hash h₁, and the Lean statement with elaborated type hash h₂, together with the definitions of every constant it uses, and the Lean statement says what the informal statement says, up to the conventions recorded on the node. The review records:

• the reviewer, the date, h₁ and h₂;
• a verdict: faithful, faithful-with-conventions (listed), or not-faithful (with a taxonomy class);
• free-text notes.

A not-faithful review has the same value as a positive one. It sends the binding back to formalize with the class and the notes.

The review packet

Review-assist builds a packet for each binding in the fidelity queue. m2 review <tag> renders it:

• the informal statement and the Lean statement side by side, the Lean one pretty-printed both with and without notation;
• the back-translation, and the judge's per-clause verdicts;
• each constant in the statement, expanded to its definition and its bound node, with that node's fidelity level;
• the battery report, the critic's concerns, the dissenting candidate clusters and how they differ;
• for a re-review after a bump, the old and new types as a diff.

The packet in m2. The package review makes the packet from the files of the last build, and m2 review <tag> shows it. The packet has the informal statement and the Lean statement side by side, the Lean statement with pp.all, each constant with its type and the nodes that bind it with their fidelity level, the battery report, and the reviews of the binding. The back-translation, the critic and the candidate clusters need the model runs of the formalize pipeline, and the old and new types need the bump data, so the packet does not show them yet. With a verdict, m2 review writes the review to reviews/XX/TAG.yaml and adds its id to the binding. It refuses a reviewer that is not a person, the author of the binding, and a statement that changed after the build. The check of rule V03 on the agent runs that a reviewer started needs the run records of M5.

Review-assist never signs. An agent cannot be a reviewer. A reviewer cannot review a binding that came from an agent run that the reviewer started (rule V03).

Independence

F3 needs one of two things:

• two independent reviews: different reviewers, neither of them the binding's author, sharing no affiliation (rule V02);
• one review plus an independent formalization proved equivalent. The second formalization comes from a different run, of a different model family, given no access to the first candidate. The equivalence is proved in Lean.

The second route is cheaper, and it becomes cheaper each year. It is also the route that scales. The target for each node in the undergraduate core is F3 by cross-formalization (document 02).

Throughput targets

For undergraduate-level statements, a review takes 3 minutes. Thus one reviewer-hour gives 20 F2 reviews. The undergraduate core (about 25,000 statements and definitions, document 18) then needs about 1,250 reviewer-hours for F2. That is a summer of work for twenty people, or a year of light work for a hundred. Research-level statements take much longer, at about 15 minutes or more. For this reason the fidelity queue is ranked by unlock. Also for this reason, the Annals-Challenge-style approach is the correct order: it formalizes statements before anyone tries to prove them. A reviewed statement has more value than an unreviewed proof.

10.7 Statements without proofs

Many of the most useful formal bindings in math2 will have no proof for a long time. These are research-level theorems, open conjectures, and results whose proofs depend on large theories that Mathlib does not have. Such a binding is match: partial until a proof exists. It is still worth having:

• it can be reviewed to F2 and F3, which makes it a trustworthy target for anyone, human or agent, who wants to prove it;
• it gives search a formal type to match against (14.3);
• for conjectures, it is the precondition for any AI claim of a solution to be checkable. A solution counts only against the pinned, reviewed statement. That is the lesson of every 2025 to 2026 episode in which an AI proved the wrong version.

The formal-conjectures repository and the Annals Challenge are the two largest collections of formal statements without proofs. math2 aligns to both (document 09). If their maintainers have reviewed an aligned statement, math2 records it as a review and names the source.

10.8 Measuring fidelity

Fidelity levels are claims too, and math2 measures how reliable they are:

• Sampled re-review. Each month, a different reviewer does a blind re-review of 1% of F2 bindings and 0.5% of F3 bindings. We adjudicate and publish the disagreements. The measured error rate per level, by area, is a headline number in the notes of each release. m2 review sample draws the sample with a seed and records it in registers/samples.reg, and m2 review measure gives the rate.
• Battery evaluation. We evaluate each check in 10.4 against a labelled set of known misformalizations. The set starts from the published benchmark audits and grows with each not-faithful review. We publish detection rates per class (17.3).
• Downstream evidence. Sometimes the proof of a statement needs a hypothesis that the informal statement does not have. Sometimes the proof is suspiciously short. In both cases, the statement goes back to the fidelity queue with a flag. A suspiciously short proof means that the measured size is much smaller than that of comparable proofs.

If F2 means "probably right", math2 should be able to say how probable.

Markdown · Source · Edit