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

On September 4, 2026, Anthropic announced that Claude completed the first end-to-end, step-by-step computer-verified formalization of Fermat's Last Theorem in Lean — in 11 days. The project wrote about 13 million lines of Lean code, proved roughly 30,300 theorems (with 29,500 entering the final proof), and consumed around 6 billion output tokens. The proof route followed the Darmon–Diamond–Taylor simplification of Wiles' 1995 proof, and Lean verified it using only three standard axioms. The project was led by Anthropic researcher Tianyi Peng, using the open-source platform Prove2Me, developed with his Columbia University team — it records theorems as a directed acyclic graph (DAG), letting dozens of Claude agents work in parallel without losing project state. The same week, three consumer-grade Claude Max subscriptions completed the formalization of the Vinogradov three-primes theorem in 3 days.

📜 A 350-Year-Old Conjecture, Formalized in 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 which this margin is too narrow to contain."

Mathematicians today generally believe that any such proof was almost certainly wrong — the techniques needed were only built 358 years later by Andrew Wiles and Richard Taylor in 1994–1995. The 129-page paper spans algebraic geometry, number theory, harmonic analysis, and commutative algebra, and a critical gap found during refereeing took Wiles and Taylor a full year to repair.

A Lean formalization translates that 129-page proof line by line into machine-verifiable language — not read by humans, but checked by a tiny trusted kernel.

Kevin Buzzard of Imperial College London launched an EPSRC-funded five-year community project in 2024 to formalize Fermat's Last Theorem in Lean, recruiting mathematicians worldwide and publishing an 86-page blueprint. The community's consensus: this was a multi-year endeavor.

Claude did it in 11 days.

🧰 Why the First Attempt Failed — and How Prove2Me Rescued It

The project did not go smoothly at first. Anthropic's research post is candid:

• Early attempts with the standard Claude Code multi-agent harness failed;
• The cause was not the model but the architecture: with 13 million lines of code and tens of thousands of intermediate theorems, no single agent's context window could hold the entire project state;
• Multiple agents without shared external state would duplicate work, overwrite each other, and lose track of what remained to be done.

The solution was Prove2Me, an open-source collaboration platform built for long-horizon AI formalization:

| Mechanism | Problem it solves | |---|---| | 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, and pending | | Failure archiving | Dead ends are kept for future rounds |

Key numbers from the Prove2Me run:

• 11 days wall-clock (dozens of agents running in parallel, not one agent for 11 consecutive days);
• ~6 billion output tokens, with the model roughly corresponding to Claude Fable 5.1;
• Failed early attempts contributed ~7% of the final proof's non-boilerplate code — not a total loss;
• The final Lean-verified proof is more than 5x the size of Mathlib.

📐 What It Proved — and What It Did Not

It is important to draw this line precisely:

• It did not prove that "Claude discovered the proof of Fermat's Last Theorem." That was Wiles, 1995.
• It did show that Wiles' human proof can be automatically translated into a machine-verified Lean form.
• The route followed the Darmon–Diamond–Taylor simplified restatement.
• Lean verified it with its own three standard axioms, no additional assumptions.
• A comparator confirmed the theorem statement aligns with Mathlib's own FLT statement.

Kevin Buzzard wrote after reviewing:

> "The Anthropic researchers say it took just 11 days — this extraordinary formalization achievement proves Fermat's Last Theorem with no assumptions beyond mathematical axioms."

He added: "If automatic formalization of FLT works today, then we've taken a major step toward automatic formalization of the modern mathematical literature. These techniques will bring new tools for finding errors in the existing corpus and easing the burden on referees."

Number theorist Daniel Litt (University of Toronto) put it more directly: "If they can formalize Fermat's Last Theorem, then they can probably formalize anything."

⚖️ Same-Week Comparison: Vinogradov's Three-Primes Theorem in 3 Days on 3 Consumer Subscriptions

Anthropic's post also disclosed a controlled experiment:

• 3 consumer Claude Max subscriptions;
• Run on Prove2Me for 3 days;
• Completed the formalization of Vinogradov's three-primes theorem — every sufficiently large odd number is the sum of three primes.

While less dramatic than FLT, it is a core result in analytic number theory, and the 3-day result shows the LLM-formalization pipeline is now affordable at consumer hardware + subscription level.

🧭 The Broader AI × Math Landscape That Week

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

Frontier models + formal verification + public Lean certificates have become a standard output format for mathematical AI. AI is not "discovering" new mathematics — it is moving proofs written by human mathematicians into a machine-readable, verifiable world.

🔁 Why It Matters: Automated Formalization Goes from Paper Promise to Repeatable Engineering Output

For a decade, automated theorem proving/formalization mostly stayed at demo level. The core change here is infrastructure like Prove2Me — cutting formalization into a DAG so dozens of agents can collaborate in parallel without losing state. With that infrastructure in place, the bottleneck shifts from humans to compute + coordination, and Claude Fable 5.1 / Max subscriptions can already bring that compute cost down to community-project scale.

Lines worth tracking:

• Mathlib integration: folding some of the 29,500 intermediate theorems into Mathlib still requires substantial manual work by Buzzard's community;
• Domain expansion: PDEs, manifold learning, quantum field theory, and other subfields rarely touched by machine assistance;
• Peer review: whether AI-generated proofs can enter human review pipelines undisclosed, with new "machine-trusted + human-trusted" endorsement protocols;
• Error scanning: Buzzard's point about finding errors in the existing corpus — automated formalization may one day flag widely cited results with 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. AI Base: Mathematical Milestone in the AI World — Claude Achieves End-to-End Formalization, 2026-09-04 5. AI Weekly: Claude formalized Fermat's Last Theorem in 11 days, 2026-09 6. Kevin Buzzard's official review statement on the Anthropic research post 7. Nankai University: Formal verification of the 3D viscous Kakeya conjecture (with ByteDance Seed-Prover), 2026-09-09