Claude produces the first complete machine-checked proof of Fermat's Last Theorem in Lean, in 11 days
Anthropic reported that a Claude model (roughly comparable to Claude Fable 5.1), running for 11 days (7–18 Aug 2026) using the Prove2Me multi-agent platform, produced a complete Lean formalisation of Fermat's Last Theorem using only Lean's three standard axioms: about 13 million lines and 30,300 theorems, over 5× the size of Mathlib.
Key facts
- Run 7–18 Aug 2026; published 4 Sep 2026
- ~13M lines of Lean; 30,300 theorems (29,500 used); ~6 billion output tokens
- Only occasional high-level instructions from Anthropic researcher Tianyi Peng (e.g. 'Jacobian as a scheme sounds high priority')
- Checked against Mathlib's statement of FLT with a comparator; no axioms beyond Lean's standard three
- Kevin Buzzard (who leads the human FLT formalisation project): 'This extraordinary autoformalization achievement ... proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics.'
Science result
- Field
- mathematics / number theory / formal verification
- Problem
- Formal verification of Fermat's Last Theorem (Wiles 1995)
- Result
- First complete machine-checked proof of FLT from the axioms, in Lean 4.
- AI system
- Claude (research model comparable to Fable 5.1)
- Human role
- Near-autonomous; occasional high-level guidance
- Verification
- Formal proof in Lean
- Status
- confirmed
- Why surprising
- Buzzard's human-led project had expected to need many years to reach a full formalisation; an AI did it in 11 days.
What happened
An agentic Claude, orchestrated through the Prove2Me platform, wrote the missing chain of Lean on top of Mathlib, through the modularity-lifting machinery of the Wiles–Taylor proof, up to FLT itself.
Why it matters
Formalising FLT had been a flagship multi-year human project. Its completion by AI shows that even the deepest modern proofs can now be machine-checked at AI speed.
Changelog
- 2026-09-29: added post link(s) (1) from Google/DeepMind + math posts pass
- 2026-09-29: created
- 2026-09-29: added post link(s) (1) from Anthropic posts cluster
Related posts (2)
- Anthropic: Claude completes first formalized proof of Fermat's Last Theorem Anthropic @AnthropicAI · x · 2026-09-04
Announces a 13-million-line Lean 4 formalization of FLT done in 11 days, which experts had expected to take years. - FLT: Anthropic has beaten me to it Kevin Buzzard @XenaProject · blog · 2026-09-04
The leader of the human Lean FLT project confirms Anthropic's 11-day AI formalisation of Fermat's Last Theorem is real, and says it tells us 'essentially nothing' mathematically.
Related events
- Math Inc's Gauss formalises Viazovska's sphere-packing proofs in dimensions 8 and 24, fixing errors in the originals ★★★★
- Anthropic releases Claude Fable 5.1 and Claude Mythos 5.1 ★★★★★
- Claude proves more than two-thirds of Riemann zeta zeros are simple and on the critical line (up from 41.6%) ★★★★★
- Claude-written Lean proof claims the dying percolation conjecture θ(p_c)=0 in every dimension ★★★★★
Sources (4)
- officialAnthropic: Formalizing Fermat's Last Theorem
- pressAI Weekly: Claude formalized Fermat's Last Theorem in 11 days
- officialAnthropic on X: first formalized proof of Fermat's Last Theorem
- discussionKevin Buzzard (Xena Project): FLT: Anthropic has beaten me to it
id: 2026-09-04-claude-formalizes-fermats-last-theorem · updated 2026-09-29 · open in the interactive timeline