Claude Formalizes Fermat's Last Theorem in Lean in 11 Days: 13 Million Lines of Code, 29,500 Theorems

Forum topic · 小凯 · 2026-09-10

Summary

On September 4, 2026, Anthropic announced that Claude completed the first end-to-end, computer-verifiable Lean formalization of Fermat's Last Theorem in 11 days. The project produced roughly 13 million lines of Lean code, proved about 30,300 theorems (29,500 of which entered the final proof), and consumed approximately 6 billion output tokens. The proof follows the Darmon–Diamond–Taylor simplification of Wiles' 1995 proof and was verified by Lean using only three standard axioms. Led by Anthropic researcher Tianyi Peng, the effort used Prove2Me, an open-source platform that represents theorems as a directed acyclic graph, enabling dozens of Claude agents to work in parallel without losing project state. An early attempt with a standard multi-agent harness failed because no single agent's context window could hold the entire project; Prove2Me solved this with a theorem DAG, statement/proof separation, searchable natural-language descriptions, and failure archiving. In the same week, three consumer-grade Claude Max subscriptions formalized Vinogradov's three-primes theorem in 3 days. Reviewers including Kevin Buzzard called the result an extraordinary formalization achievement, noting it did not discover new mathematics but translated Wiles' human proof into machine-checkable form.

Key points

On September 4, 2026, Anthropic announced that Claude completed the first end-to-end, computer-verified Lean formalization of Fermat's Last Theorem in 11 days of wall-clock time.
The project produced roughly 13 million lines of Lean code, proved about 30,300 theorems (with 29,500 entering the final proof), and consumed about 6 billion output tokens.
The proof route follows the Darmon–Diamond–Taylor simplified restatement of Wiles' 1995 proof. Lean verified everything using only three standard axioms; a comparator confirmed alignment with Mathlib's own FLT statement.
The project was led by Anthropic researcher Tianyi Peng, using the open-source platform Prove2Me developed with his Columbia University team. Prove2Me records theorems as a directed acyclic graph (DAG), letting dozens of Claude agents work in parallel without losing project state.

Background: 350 years, then 11 days

In 1637, Pierre de Fermat wrote in the margin of Diophantus' *Arithmetica* that for integers $$n > 2$$ , no positive integers $$a, b, c$$ satisfy $$a^n + b^n = c^n$$ , adding that he had a "truly marvelous proof" the margin was too small to contain. Mathematicians today generally believe that proof, if it existed, was almost certainly wrong — the techniques needed were only developed by Andrew Wiles and Richard Taylor in 1994–1995, in a 129-page paper spanning algebraic geometry, number theory, harmonic analysis, and commutative algebra (with a key gap patched over a year of work).

Kevin Buzzard (Imperial College London) had launched a five-year, EPSRC-funded community project in 2024 to formalize FLT into Lean, publishing an 86-page blueprint and estimating it would take years. Claude finished in 11 days.

Why the first attempt failed, and how Prove2Me fixed it

Early attempts using a standard Claude Code multi-agent harness failed — not because of the model, but the architecture: no single agent's context window could hold the state of 13 million lines of code and tens of thousands of intermediate theorems.
Agents without shared external state duplicated work, overwrote each other, and lost track of remaining tasks.

Prove2Me solves this with:

| Mechanism | Problem solved | |---|---| | Theorem DAG | Each theorem is a node; dependencies are directed edges | | Statement/proof separation | Lean recompiles only changed files, not the whole project | | Natural-language descriptions | Each theorem has a searchable NL description for agent retrieval and reuse | | Multi-agent parallelism | New agents consult the DAG: what's proved, in progress, or pending | | Failure archiving | Dead ends are kept for future rounds |

Notable figures: failed early attempts contributed about 7% of the final proof's non-boilerplate code; the resulting proof is more than 5× the size of Mathlib.

What it proved — and what it didn't

It did not mean Claude discovered a proof of FLT — that was Wiles in 1995.
It did show that Wiles' human proof can be automatically translated into machine-step-verifiable Lean form.
Verification used only Lean's three standard axioms, with no extra assumptions.

Kevin Buzzard wrote after review: "Anthropic researchers say it took only 11 days — this extraordinary formalization achievement proves Fermat's Last Theorem with no assumptions beyond the mathematical axioms." He added that automatic formalization of FLT suggests an important step toward automating the formalization of the modern mathematical literature, with tools to find errors in existing work and reduce reviewer burden. Number theorist Daniel Litt (University of Toronto) put it more directly: "If they can formalize Fermat's Last Theorem, then presumably they can formalize anything."

Same-week comparison: Vinogradov's three-primes theorem

In a control experiment, three consumer-grade Claude Max subscriptions formalized Vinogradov's three-primes theorem (every sufficiently large odd number is the sum of three primes) on Prove2Me in 3 days — showing the pipeline is affordable at consumer-subscription level.

Context: the AI × math landscape that week

| Project | Date | Key numbers | Difference from FLT project | |---|---|---|---| | ByteDance Seed-Prover + Nankai (Shaoming Guo team) | 9/9 | 3D viscous Kakeya conjecture formalized, 1.8M lines of Lean, ~90% by Seed-Prover | Different team/subdomain | | FormaTheoria × Tsinghua + Shing-Tung Yau | 9/1 | 4 key CFSG theorems formalized, 994K lines of Lean | Group theory / open-sourced code | | OpenAI Astra Ten Proofs / Bel | August | 10 mathematical results formalized | Mixed discovery + formalization | | Google Antigravity Teamwork + Gemini 3.7 Flash | 9/1 | 7 open FOCS/JMLR problems solved (incl. Knuth Cycles conjecture, 40+ pages of verified Lean) | Multi-agent, different stack |

Significance

For a decade, automated theorem proving/formalization remained demo-level. This wave's core change is infrastructure like Prove2Me: once formalization tasks are cut into a DAG, dozens of agents can work in parallel without losing state, shifting the bottleneck from "people" to "compute + coordination."

Threads worth tracking:

Mathlib integration: merging useful intermediate lemmas from the 13M lines still requires substantial manual work by Buzzard's team;
Domain expansion: PDEs, manifold learning, quantum field theory, and other subfields rarely touched by machine assistance;
Review pipelines: redesigning "machine-trusted + human-trusted" dual endorsement protocols for AI-generated proofs;
Error scanning: automatic formalization may eventually reveal which widely-cited results rely on undeclared assumptions.

References

1. Nature News: Anthropic AI 'formalizes' proof of Fermat's last theorem in just 11 days, 2026-09-07 (doi: 10.1038/d41586-026-02822-9) 2. Anthropic Research Post: First complete computer-checked proof of Fermat's Last Theorem, 2026-09-04 3. Tech Times: Fermat's Last Theorem Machine-Checked — Claude Completes in 11 Days, 2026-09-05 4. Kevin Buzzard's official review statement on the Anthropic research post 5. Nankai University: 3D viscous Kakeya conjecture formalization (with ByteDance Seed-Prover), 2026-09-09