Claude formalizes Fermat’s Last Theorem in Lean — on Mathlib and Prove2Me

TL;DR

• Claude Fable 5.1 kernel-checked a 13M-line Lean proof of Fermat’s Last Theorem in 11 days.
• Anthropic’s repo credits 106 upstream files to the Imperial/Mathlib FLT effort.
• Prove2Me, a Columbia DAG orchestrator, was the actual unlock after single-agent runs trampled state.
• Three agents formalized Vinogradov’s Three Primes in 3 days on a $90/month Claude Max plan.

Today’s single research feature is a genuine milestone dressed in a misleading frame. Claude Fable 5.1 kernel-checked a 13M-line Lean formalization of Fermat’s Last Theorem in 11 days, burning roughly 6B output tokens — the kind of number that reads as pure model progress. It isn’t. Anthropic’s own repo credits 106 upstream files to the Imperial College / Mathlib community FLT effort, and the run only stopped collapsing once a Columbia-built DAG orchestrator, Prove2Me, took over from single-agent attempts that lost state and overwrote each other’s work. The follow-on Vinogradov formalization — three agents, three days, on a $90/month Claude Max plan — reinforces the same read: the model is the executor, the scaffolding and the prior human formalization are doing the load-bearing work.

Claude formalizes Fermat’s Last Theorem in Lean in 11 days

Source: anthropic-research · published 2026-09-04

TL;DR

• Claude Fable 5.1 kernel-checked a 13M-line Lean proof of Fermat’s Last Theorem in 11 days, burning ~6B output tokens.
• Anthropic’s repo credits 106 upstream files to the Imperial/Mathlib community FLT effort, denting the “autonomous” framing.
• Prove2Me, a Columbia-built DAG orchestrator, was the actual unlock after early single-agent runs lost state and trampled each other’s work.
• Three agents formalized Vinogradov’s Three Primes Theorem in 3 days on a $90/month Claude Max plan.

What Claude actually shipped

Anthropic’s internal “Claude Fable 5.1” model, driven by a Claude Code multi-agent scaffold, produced a machine-checked Lean formalization of Fermat’s Last Theorem following the 1995 Darmon–Diamond–Taylor exposition of Wiles. The Lean compiler verified the whole thing against Lean’s three standard axioms. That is a real result: a proof that took Wiles seven years and 129 pages, and that the Lean community has been chipping at for years, now compiles end-to-end.

The numbers are big and worth stating plainly: ~6 billion output tokens, 13 million lines of Lean, 30,300 lemmas of which 29,500 are load-bearing in the final proof. At retail API pricing that token spend is roughly $300K, or ~$100K at Anthropic’s internal cost — an order of magnitude below the £1M-scale multi-year grants funding equivalent human formalization work ¹.

Prove2Me did the coordination

The more interesting technical story is that Claude alone failed. Early runs saw agents “lose track of state and trample each other’s work” — the standard failure mode of long-horizon multi-agent work ². The breakthrough came from integrating Prove2Me, Tianyi Peng’s Columbia project, which externalized the proof plan into a directed acyclic graph, separated theorem statements from their proofs to cut Lean compile time, and kept natural-language descriptions searchable so parallel agents could find the right sub-goal ².

flowchart LR
    A[Human strategic guidance<br/>e.g. 'prioritize Mazur'] --> B[Prove2Me DAG<br/>theorem statements + deps]
    B --> C[Dozens of Claude agents<br/>working in parallel]
    C --> D[Candidate Lean proofs]
    D --> E{Lean compiler}
    E -->|fail| C
    E -->|pass| F[13M-line verified artifact]

Read that diagram carefully: the model is one box. The coordination layer is the rest of the system, and it is what made the token spend converge instead of thrash.

The autonomy asterisk

Anthropic’s own repository credits 106 upstream files to the Imperial College FLT project and Mathlib ³. That is not a footnote — it is years of community definitions, lemmas, and tactic infrastructure that the “autonomous” run built on. Kevin Buzzard, who leads the Imperial effort, called the result an “extraordinary autoformalization achievement” but flagged that Claude tackled the older Darmon–Diamond–Taylor exposition, not the modern Khare–Taylor proof his EPSRC-funded team is targeting ⁴. His verdict: human effort remains “essential.”

Critics go further on the artifact itself. At ~13M lines, an estimated 2.5M of which are repetitive boilerplate, the proof is being called “write-only” code that swaps one hard verification problem (peer-reviewing Wiles) for another (auditing an AI-generated codebase 5× the size of Mathlib) ⁵.

The cost floor is the real story

The FLT headline will get the clicks, but the load-bearing datapoint is the side experiment: three agents formalized Vinogradov’s Three Primes Theorem in three days on consumer Claude Max subscriptions ⁶. If that generalizes, the barrier to serious formalization work drops from a multi-year grant to a $90/month plan and a good DAG. That, not the token count on FLT, is what changes who gets to formalize what.

Footnotes

1. 36Kr (EN) — https://eu.36kr.com/en/p/3969755274883328

   At retail API rates the six billion output tokens represent roughly $300,000 of compute; with a ~70% gross margin the true cost to Anthropic is closer to $100,000 — versus the £1M-scale multi-year grants awarded for human formalization projects.

   ↩

2. dev.to (jamilxt) — ‘AI agents failed… then they got a shared to-do list’ — https://dev.to/jamilxt/ai-agents-failed-to-prove-fermats-last-theorem-then-they-got-a-shared-to-do-list-h0k

   Early Claude attempts failed as agents ‘lost track of state and trampled each other’s work’; success only came after Prove2Me externalized state into a shared DAG acting as collective memory for dozens of parallel agents.

   ↩ ↩²

3. dev.to (alifar) — ‘The community project and Claude’s real role’ — https://dev.to/alifar/fermats-last-theorem-in-lean-the-community-project-and-claudes-real-role-2e13

   Anthropic’s repository credits 106 upstream files to the existing community FLT project at Imperial College London and to Mathlib, undercutting the ‘fully autonomous’ framing in press coverage.

   ↩

4. Techstrong.ai — https://techstrong.ai/articles/anthropics-claude-agents-formalize-fermats-last-theorem-in-11-days/

   Kevin Buzzard called it an ‘extraordinary autoformalization achievement’ but noted Claude followed the 1995 Darmon–Diamond–Taylor exposition of Wiles, not the modern Khare–Taylor proof his own EPSRC-funded project is targeting — so the human effort remains ‘essential’.

   ↩

5. ExplainX analysis — https://www.explainx.ai/blog/anthropic-claude-fermats-last-theorem-lean-proof-2026

   The 13M-line artifact is roughly five times Mathlib and contains an estimated 2.5 million lines of repetitive boilerplate; critics call it ‘write-only’ code that swaps one verification problem (peer review) for another (auditing AI-generated codebases).

   ↩

6. AIWeekly — https://aiweekly.co/alerts/anthropics-claude-formalizes-fermats-last-theorem-in-lean

   As a secondary benchmark, three Claude agents formalized Vinogradov’s Three Primes Theorem in three days using consumer-tier Claude Max subscriptions — suggesting the barrier to entry for serious formalization may collapse to a $90/month plan.

   ↩