Claude Formalized Fermat's Last Theorem in Lean in 11 Days
Anthropic reports that Claude formalized Fermat's Last Theorem in the Lean proof language, working largely autonomously for 11 days. The result is roughly 13 million lines of machine-checked Lean proving about 30,300 theorems, verified against Lean's three standard axioms. Mathematician Kevin Buzzard, who leads the human FLT formalization project, reviewed and endorsed the proof.
On this page
An 11-day, 13-million-line proof
Anthropic published the write-up on September 4: Claude, running in a multi-agent harness, formalized Fermat's Last Theorem in the Lean programming language over roughly 11 days of largely autonomous work. The artifact contains about 13 million lines of Lean, more than five times the size of Mathlib, the standard Lean mathematics library, and it proves approximately 30,300 theorems, of which 29,500 are used in the final argument. Lean verified the result using only its three standard axioms, and a comparator confirmed the formal statement matches Mathlib's own statement of the theorem. The proof is on GitHub. [1]
This is not a new proof of Fermat's Last Theorem. It is a full formalization of the existing proof strategy, following the simplified exposition by Darmon, Diamond, and Taylor rather than Wiles's original paper. Formalizing means translating a human proof into a machine-checkable language, which is famously tedious: a community project led by Imperial College London's Kevin Buzzard has been formalizing FLT since 2024 and is still short of done. [1] [3]
How the Prove2Me platform kept agents on track
The workflow ran on Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and collaborators at Columbia University. It maintains a directed acyclic graph of theorem statements so agents always know what to prove next, splits statements from proofs into separate files to keep compilation fast, and stores natural-language descriptions so results can be searched and reused. A Claude Code-based harness coordinated dozens of agents defining concepts and proving progressively harder statements, consuming around 6 billion output tokens from an internal research model described as roughly comparable to Claude Fable 5.1. [1] [3]
Early attempts failed when agents lost track of project state; those runs still contributed about 7 percent of the non-boilerplate lines in the final proof. [1]
Humans set priorities, then got out of the way
Human involvement was limited to occasional direction from Peng. "Jacobian as a scheme sounds high priority," reads one instruction; another asked for the Mazur theorem to be prioritized. Otherwise the agents ran on their own, logging their own milestones. When the proof completed, one entry read "Historic moment (modulo re-check)." [1]
Buzzard reviewed the result and called it an "extraordinary autoformalization achievement," noting that it "proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics" and that AI autoformalization artifacts are now robust enough to build on. Community discussion of the result has been active, with particular attention to how much of the achievement belongs to the multi-agent platform rather than raw model reasoning. [1] [4]
Why formal proofs matter now
The significance is less about Fermat, whose proof has been accepted since 1995, and more about verification. Machine-checked proofs rule out gaps that peer review can miss, and Anthropic argues that as AI starts contributing research mathematics, formalized proofs may be the only feasible way for humans to keep up with what models produce. Writing Lean also appears to help the models themselves: in a follow-up, three Claude Max plans formalized Vinogradov's Three Primes Theorem in three days using the same platform. [1]
The caveats are worth stating plainly: the proof leans heavily on Mathlib, is likely far longer than it needs to be, and the effort was extremely token-intensive. It is a milestone for verification and autonomy, not a mathematician replacement. [1]
Sources
- Formalizing Fermat's Last TheoremAnthropic
- Anthropic's Claude formalizes Fermat's Last Theorem in LeanAI Weekly
- Buzzard's formalization of Fermat's Last Theorem (community project)Imperial College London
- Discussion: formalizing Fermat's Last TheoremHacker News