Claude formalizes Fermat's Last Theorem (September 5) — 13 million lines in 11 days
Anthropic said on September 5, 2026 that Claude had, for the first time, formalized Fermat's Last Theorem end to end in the Lean proof assistant — producing a complete proof a machine can check line by line. The work ran for eleven days, largely autonomously, and generated roughly 13 million lines of Lean code along the way. It proved 30,300 theorems, of which 29,500 were used in the final proof, and consumed about six billion output tokens. The first attempt failed; the run only completed after a harness built on Prove2Me, an open-source tool from a Columbia University group, was added partway through. Anthropic states plainly that the result stands on community infrastructure the company did not build: Kevin Buzzard's Fermat's Last Theorem formalization project at Imperial College London, and Mathlib, Lean's mathematics library. One distinction has to be kept straight. The person who proved the theorem was Andrew Wiles, in 1994. What Claude did was render that proof into a form a machine can verify — a task experts had expected to take many years
The three lines
- Result — the first end-to-end, machine-checkable formalization of Fermat's Last Theorem in Lean, in 11 largely autonomous days
- Scale — about 13 million lines of Lean, 30,300 theorems proved (29,500 used), roughly 6 billion output tokens
- Distinction — Wiles proved it in 1994. This run translated that proof into something a machine verifies line by line
Key questions
- Did Claude prove Fermat's Last Theorem
- **No. Andrew Wiles proved it in 1994. What Claude did was formalize that proof.** The distinction is easy to lose from a headline, so it is worth setting down first. | Stage | Who | What | |---|---|---| | **Proof** | Andrew Wiles (1994) | built a mathematical argument for human readers | | **Formalization** | Claude (2026) | rendered that argument as code a machine **checks line by line** | **Formalization is not transcription, though.** A human paper leaps over steps with words like *obvious*, *similarly*, *details left to the reader*. Formalization means filling in **every one of those omitted steps**. For a theorem whose principal paper runs past a hundred pages and rests on a large share of twentieth-century number theory, the number of gaps to fill runs into the tens of thousands. **That is what 30,300 proved theorems represents.** Why formal proof exists as a device is set out separately (「What formal proof is」).
- How was eleven days possible
- **Three pieces already existed, and a fourth was added mid-run.** | Component | Built by | Role | |---|---|---| | **Mathlib** | the Lean community | mathematics library; foundational results already formalized | | **Buzzard's FLT project** | Kevin Buzzard, Imperial College London | the blueprint and existing progress | | **Lean** | Lean developers | the proof assistant itself | | **Prove2Me** | Columbia University (Tianyi Peng's group) | **the harness added partway through** | **That Anthropic published this list itself is the notable part.** The company states the result rests on infrastructure it did not build. **So the accurate sentence is not 'Claude did it alone' but 'Claude ran eleven days along a road other people spent years laying.'** And **the first attempt failed.** Completion came only after the Prove2Me-based harness was attached mid-run. Tianyi Peng is an Anthropic researcher who also leads the Columbia group.
- How much compute is six billion tokens
- **Priced at commercial API rates it becomes legible.** Applying a recent frontier output price of roughly $20 per million tokens (「GPT-5.6 Sol cuts API prices (August 21)」·「What AI token pricing is」) gives **6 billion × $20/million ≈ $120,000**. Anthropic ran its own model on its own infrastructure, so this is not a bill — it is a rough gauge of **what the same work would cost from outside.** | Item | Value | |---|---| | Duration | **11 days** | | Lean code generated | ~**13 million lines** | | Theorems proved | **30,300** (used: **29,500**) | | Output tokens | ~**6 billion** | | Commercial-rate equivalent | ~**$120,000** | **The ratio worth noticing is 30,300 to 29,500.** **97.4 percent of what was proved ended up in the final proof.** Only 2.6 percent was discarded, which suggests the run worked backwards from the goal to the lemmas it needed rather than exploring blindly. **Whether those 800 unused results were waste or the normal cost of search cannot be judged from what has been published.**
"AI proved Fermat's Last Theorem" is the wrong sentence. Wiles proved it in 1994. What happened here is a different thing, and the different thing is more interesting.
1. What was announced
Anthropic said on September 5, 2026 that Claude had formalized Fermat's Last Theorem end to end in the Lean proof assistant — the first time a complete, machine-checkable version has existed.
| Item | Value |
|---|---|
| Duration | 11 days (largely autonomous) |
| Lean code generated | ~13 million lines |
| Theorems proved | 30,300 |
| Used in the final proof | 29,500 (97.4%) |
| Output tokens | ~6 billion |
2. Proving and formalizing are different acts
| Stage | Who | What |
|---|---|---|
| Proof | Andrew Wiles (1994) | an argument for human readers |
| Formalization | Claude (2026) | code a machine checks line by line |
Formalizing is not dictation. Human papers skip steps with obvious, similarly, details left to the reader. Formalization fills every one of them.
Wiles's paper runs past a hundred pages and presumes a large slice of twentieth-century number theory beneath it. Thirty thousand gaps is what that comes to — which is what the theorem count measures. Why formal proof exists as a device is set out separately (「What formal proof is」).
3. Claude did not do this alone
Anthropic states that the result rests on infrastructure the company did not build.
| Component | Built by | Role |
|---|---|---|
| Lean | the Lean community | the proof assistant |
| Mathlib | the Lean community | mathematics library — foundational results already formalized |
| FLT project | Kevin Buzzard, Imperial College London | blueprint and prior progress |
| Prove2Me | Columbia University, Tianyi Peng's group | harness added after the first attempt failed |
The first attempt failed. Completion followed only once the Prove2Me-based harness was attached mid-run. Publishing both the failure and the external dependence is not the usual shape of an AI results announcement.
4. Why this matters
It is a route to trusting AI-generated mathematics without reading all of it. Every time AI has touched an open problem, the question that followed was who checks this (「AI took a run at ten unsolved maths problems」). Formal proof answers that mechanically. If Lean accepts the code, there is no logical gap, whether or not a human reads a line of it.
And the speed carries meaning. Experts had expected this formalization to take years; eleven days is a different order of magnitude. But it is eleven days on top of already-laid infrastructure. The years poured into Mathlib and Buzzard's project are not inside that number.
5. What remains unresolved
- The technical report was not read directly. Figures come from coverage.
- The scope of "largely autonomous" is unclear — intervention count and character are not stated.
- Independent review by outside mathematicians, and any Mathlib merge plan, could not be confirmed.
- The ~$120,000 estimate is this article's, not a disclosed cost.
- Announcement dates differ across outlets (September 4 versus 5).
- In the same week, OpenAI recorded that its own model had become harder to monitor (「GPT-6 Astra's system card」). One track opened a way for machines to verify AI reasoning; the other closed a way for humans to read it.
Sources
- Anthropic — Formalizing Fermat's Last Theorem
- Anthropic — Formalizing Fermat's Last Theorem in Lean (technical report PDF)
- SiliconANGLE — Anthropic uses Claude to formalize proof of Fermat's Last Theorem
- AI Weekly — Claude formalized Fermat's Last Theorem in 11 days: Anthropic
- AI Weekly — Anthropic's Claude formalizes Fermat's Last Theorem in Lean