Fermat's Last Theorem in Lean: Lessons for Multi-Agent Coding

On September 4, Anthropic published Formalizing Fermat's Last Theorem, describing the first end-to-end, computer-checked proof of the theorem, verified in Lean. A team of Claude agents, running on a Claude Code-based multi-agent harness and an internal research model the post calls roughly comparable to Claude Fable 5.1, produced it in 11 days, largely autonomously. I can't judge the mathematics. I can judge the engineering, because the setup is a scaled-up version of what I do daily: several coding agents on one codebase, with a machine deciding what counts as done.

What was actually shipped#

From the post and the open-source repository:

• About 13 million lines of Lean, over 5x the size of Mathlib, the main community math library.
• 30,300 theorems proved, 29,500 of them used in the final proof.
• Roughly 6 billion output tokens.
• Lean 4.33.1 on Mathlib v4.33.0, Apache 2.0, depending only on Lean's three standard axioms, with no sorry or native_decide.

Beyond the build itself, where the Lean kernel checks every declaration, two more checks ran: a comparator that matched the statement against one written using only Mathlib and replayed the proof through the kernel, and nanoda, an independent Rust kernel that checked 1,052,234 declarations.

The early failure is the useful part#

Early attempts failed because agents "quickly lost track of the project's state and stopped collaborating effectively." The fix the post describes was not a better model. It was shared state.

That fix was Prove2Me, an open formalization platform from Tianyi Peng and collaborators at Columbia. It:

• Kept a directed acyclic graph of theorem statements that agents used to pick what to prove next.
• Stored statements and proofs in separate files, with the links kept independently, which sped up compilation.
• Kept a natural-language description of every statement so agents could search for and reuse existing results.

The post says the DAG helped with memory degradation and let multiple agents work in parallel. Parallel coding agents fail the same way at smaller scale. Not because they can't write code, but because two of them rebuild the same helper, or one works from a stale picture of what is done.

A checker that doesn't negotiate#

Lean is why 13 million generated lines are worth anything. A proof compiles or it doesn't, and nobody has to be persuaded. The repo also names the limit: no tool checks that an intermediate theorem means what its name suggests.

Software has weaker versions: the type checker, contract tests, schema validation, CI that blocks merges. Make those gates the thing agents are graded against, not a human skimming a diff at the end of the day. Quorate, the review CLI I maintain, follows the same instinct: several AI reviewers, then a deterministic PASS/WARN/FAIL gate. The FLT repo goes further: #guard_msgs wraps #print axioms, so the build fails if the proof rests on anything beyond the three standard axioms. The software equivalent is a CI step that fails when someone adds a @ts-ignore, a skipped test, or a new any to a critical path.

Contracts before implementations#

Splitting statements from proofs is the part I would copy literally. In the repo, Theorems/ holds statements, P2M/Sol/ holds proofs and Definitions/ holds definitions, and each proof imports the statements it cites. The statement is the contract. Any proof that satisfies it is acceptable.

In a codebase, that means interfaces, API schemas and typed signatures reviewed first, as their own unit, with implementations fanned out to agents afterward. The natural-language index maps to something most teams lack: a searchable description of what each module already does, so an agent finds the existing date parser before writing a fourth one. Reuse ran outward too: the proof adapts pieces from Kevin Buzzard's Imperial College London FLT project and flt-regular.

What I'd check on Monday#

• Is task state explicit? A dependency graph or task file agents read and update, not state living in each agent's context.
• Are contracts reviewed separately? Interface and schema changes get their own review before implementation PRs.
• Does your gate trust nothing? If the only check is "another model looked at it", you don't have a gate.
• Can agents find what exists? A maintained module index beats hoping retrieval gets lucky.

My take#

The post is candid about costs. The proof is "likely much longer than it needs to be," the project was token-intensive, failed attempts still make up about 7% of the non-boilerplate lines, and the repo notes that names are machine-generated and the statements are what count. Agent output in a product codebase looks similar: correct against the checker, verbose, hard to maintain. A formal proof can afford that because, as the repo puts it, it is written to be checked rather than read. Most software can't.

So this doesn't tell me to hand a backlog to a swarm. It tells me where to invest before adding agents: shared state, contracts, and a checker that can't be talked around. Anthropic also reports agents on three personal Claude Max plans formalizing Vinogradov's Three Primes Theorem in three days through Prove2Me, and argues the right scaffold makes such work achievable on consumer subscriptions. I think the same holds for software teams.