The checker audits proofs,
not statements

Lean is a proof assistant: mathematics is written as code, and a small trusted core called the kernel checks every inference. Lean represents a statement as a type and its proof as a term of that type. If any inference fails, the file does not compile.

This separates two objects that ordinary mathematical prose often presents together. One of them, the statement, is the formal version of what is to be proved; the other, the proof, is the code that establishes it. A sorry left in a proof marks a step skipped for now, so a proof that still contains sorry is unfinished.

The completed Fermat formalization contains no sorry and depends on exactly the three standard axioms built into Lean: propext, Classical.choice and Quot.sound. Depending only on those axioms means that the formalization introduced no additional foundational assumptions. FinalCheck.lean makes this a build condition through #print axioms: an unexpected or missing axiom causes the build to fail.

The kernel’s guarantee stops at the formal statement placed before it. The Prove2Me paper states the boundary directly: The proof kernel certifies that a proof inhabits a statement, but not that the statement faithfully captures the intended claim.

An AI-generated statement can omit a hypothesis, drift away from the source mathematics, or even say something vacuous. If the submitted proof establishes that weakened statement, the kernel will still accept it. The proof repository’s README describes the same boundary: What no tool can check is that each intermediate theorem means what its name suggests; that is for the reader to judge.

The checker therefore audits proofs, not statements. It can establish that the code proves exactly the Lean declaration it was given. It cannot establish that the declaration says what its natural-language label, source theorem or surrounding project intended it to say.

The Prove2Me paper cites a 2026 Lean-as-judge audit by Bourigault and colleagues. In that study, only about 43% of the proved statements were found faithful to the original claims. This was not a measurement made by the Prove2Me authors themselves or a statistic from the FLT project.

The paper does not respond by asking humans to read every generated proof. Instead, it narrows human review to definitions and top-level statements. That still leaves a coordination problem: dozens of agents must write and reuse statements without turning one shared project into many incompatible local proofs.

Prove2Me was designed by Tianyi Peng, an Anthropic researcher and assistant professor at Columbia Business School, together with collaborators at Columbia University. Its basic move is simple: separate each theorem statement from the proofs submitted for it. The statement becomes a standalone object that cannot be edited after submission. Different agents can then submit multiple proofs of the same target.

Work on the platform happens in theorem cards. Each card has three core fields. Description explains the task in ordinary language. Preamble lists the Lean imports that define its environment. Formal statement stores the Lean declaration and ends in := by sorry, showing that the card does not yet contain a proof. A complete submission can also include a Source link, Tags, and a selected verification environment.

A proof submission supplies a theorem named solution. Its type must match the target exactly. It may contain no sorry and may add no axioms. The platform compiles the proof in the target’s environment and checks that the type of solution and the card’s statement are interchangeable. A solution can also disprove a card by having the type of the target’s negation. Every proof includes a natural-language explanation of its approach.

Cards sit in a DAG, or directed acyclic graph. This is a network of one-way dependencies in which no theorem can eventually depend on itself. A proof-sketch may import other statements on the platform, including statements that are still open. It proves the parent theorem on the condition that those imported results hold. Each imported result becomes another card in the graph.

Property 1 in the paper defines how the pieces combine: a theorem is verified when every child lemma imported by its proof has been verified. Because statements and proof-sketches cannot be edited after submission, accepted local proofs can be combined without their targets changing underneath them.

Each child lemma is also a self-contained problem. An agent can work on one card without downloading or compiling its parent. When every child closes, the parent closes automatically. The process repeats until every leaf in the dependency graph has been proved.

Anthropic’s blog summarizes three benefits observed in the FLT run. The theorem DAG gave agents shared state for choosing what to attempt next, mitigating memory degradation while permitting parallel work. Keeping statements and proofs in separate files, with their links maintained independently, reduced compilation and resource costs. Natural-language descriptions made statements searchable and reusable, producing a simpler proof path. The paper supplies the platform mechanisms behind those observations: the card ledger and proof-sketch graph, the statement/proof split, and description-based search.

Decomposition alone does not make decentralized contributions agree. Prove2Me therefore organizes a project as a mission. Its core contains a headline goal theorem, the definitions needed to state it, and milestone lemmas that define the route. The human who proposes the mission is called the captain and need not be a Lean expert.

A milestone pairs an authoritative natural-language statement, usually copied from the source, with the Lean theorem that the captain has approved as its canonical formalization. The paper sets two requirements for milestones. They must be idempotent: independent attempts should converge on the same target rather than create incompatible restatements. They must also be authoritative: downstream work can import the target without repeating the semantic audit.

An agent assigned to a milestone formalizes against its established statement instead of inventing another version. If the linked theorem has already been proved, the agent reuses it instead of proving the result again. Proof-sketches connect the milestones. Once every milestone is proved and those connections close, the headline goal resolves through the graph.

Human review is concentrated at the mission core. Before release, people check the goal, its definitions, and the milestone statements against the intended mathematics, and audit nothing beyond it. Agents can add any number of intermediate lemmas without human review.

The paper’s argument is that the system does not have to trust an agent’s choice of decomposition. It relies on humans having approved the core statements and on the Lean kernel accepting their proofs. Intermediate lemmas matter only because they help close those audited targets.

A captain can ask an agent to draft the mission proposal, including its formal declarations. The paper says the final audit cannot be delegated: the human is required to click each statement individually to confirm it.

Prove2Me reduces the Lean knowledge needed for that review with an independent read-back. An auditor agent receives only a Lean declaration and its dependent definitions. It does not see the source statement. The agent translates the declaration back into ordinary mathematics, and the human compares that translation with the intended claim.

The platform’s search API indexes the natural-language card descriptions. Agents are instructed to search before submitting, reuse an existing theorem when one is available, and introduce a new statement only when none exists. A statement earns credit when later proofs import it, providing the platform’s form of citation. Accepted results accumulate in a reusable library called Formalpedia. Agents also have a discussion channel where they post progress, intermediate findings and lessons learned in real time.

One episode in the paper’s Sensitivity Conjecture mission, which followed Hao Huang’s 2019 proof and which the paper reports as closed with all four of its milestones reached, shows these mechanisms interacting. An agent submitted a proof-sketch that imported a theorem named gotsman_linial. Another agent disproved that statement. The first then proposed gotsman_linial_with_zero, adding the missing boundary condition, and the corrected theorem closed the entire branch.

For the FLT mission, the milestone graph has three colored blocks, labeled in the figure itself as Mazur (irreducibility of the Frey curve’s mod p representation), Ribet (level lowering) and Wiles (modularity of semistable curves). Their branches converge on “No Frey package exists,” then on Fermat’s Last Theorem; a Frey package, in PROOF-PATH’s terms, is a normalized counterexample together with the Frey curve built from it. In platform terms, the blog’s DAG is the immutable statement ledger joined by proof-sketches; its separate files are the statement/proof split; and its reusable descriptions are the search layer over the same ledger.

The agents immediately drew a boundary around that label. At 10:01 pm, one saw no open leaf beneath the root and began polling the root directly. At 10:02 pm, another wrote Before posting: verify myself with an independent GET. A third called it a Historic moment (modulo re-check). At 10:04 pm, another agent saw that the root’s only direct child now read Proved. It told itself Don't jump to conclusions and checked the cards one by one.

At 10:25 pm, a team member asked whether the whole theorem had now been formalized. The responding agent separated what the platform had established from what still remained unchecked.

Proved on Prove2Me meant that roughly 30,000 cards in the dependency tree each had a machine-checked Lean proof against the statements of their children. It did not yet mean that the entire tree had been fetched and recompiled independently. The team had not yet matched every proof type against its card again, confirmed that the axioms were limited to Lean’s standard three plus each card’s declared children, or checked that the whole graph was acyclic and grounded.

The agent’s conclusion was exact: Until the re-check reads clean the honest sentence is "proved on prove2me, pending the independent re-check" rather than "FLT is formalized".

The distinction follows from how Prove2Me checks each card. A card’s proof is compiled independently against the statements of its children. A Proved mark records the successful composition of those local checks. Rebuilding the complete artifact from end to end is a separate step.

The morning after the run, the team recompiled all 29,511 cards from source outside the platform. The following day it assembled the dependency tree as a single Lean project. According to the repository’s build ledger, the Lean kernel checked all 60,475 modules. A clean build took 5 h 32 min with 96 parallel jobs and reached a peak memory use of 153 GB.

Two further judges checked the result. The first was the comparator tool from the Lean ecosystem. It verified that the proved statement was identical to a reference statement importing only Mathlib. It also checked that no additional axioms were used and replayed the complete proof, including Mathlib, through the kernel. Its verdict was Your solution is okay! The run took 14 h 46 min and peaked at 230 GB.

The second was nanoda, an independent implementation of the Lean kernel written in Rust. It accepted an export of the same environment and reported Checked 1052234 declarations with no errors.

Anthropic used four small patches with nanoda. One added progress output, while three accelerated definitional-equality search. The README states that none of them adds, removes, or weakens a typing rule.

Buzzard then performed his own pass, compiling the code base and running the comparator tool. His conclusion remained it checks out. He described the artifact as over 13.4 million lines and said that, on a 96-core machine, it took nearly 20 times as long to compile as Mathlib.

Anthropic describes FLT as a token-intensive project. It consumed about six billion output tokens and produced what the blog calls the largest Lean proof ever constructed. The blog does not provide a unit price for those tokens.

A smaller experiment used three personal Claude Max plans, with the agents collaborating entirely through Prove2Me. They completed a formalization of Vinogradov’s Three Primes Theorem, which the blog files under applications of the Hardy-Littlewood Circle Method, in three days. Anthropic’s judgment was: We think with the right scaffold, collaborative formalization of major results with consumer AI subscriptions is achievable.

Table 1 of the Prove2Me paper places this beside two other case studies. A centralized swarm used metered API inference and Anthropic’s Opus 4.5 model. It spent about $100,000 on 30,000 agent runs and took 7 days to formalize an algebraic combinatorics textbook, producing 130K lines of Lean source.

On Prove2Me, 6 agents using two consumer subscriptions formalized the Bandit Algorithms textbook, producing 151K lines of Lean source. The run took 13 days and cost about $400.

The paper does not present these rows as a controlled experiment. Metered API usage and subscriptions use different cost conventions, so the figures are not directly comparable. Each row also combines two changes: a newer model generation and a harness designed for multi-agent proving. Separating their effects would require holding the model fixed while changing only the harness. The paper leaves that experiment to future work.

Buzzard set the FLT run against the £1M over 5 years supporting his own project. Anthropic took 11 days, he wrote, but I do wonder if they spent more money. Neither the six billion tokens nor that remark supplies a conversion.