Fermat’s Last Theorem has been true since 1995, when Andrew Wiles closed a 358-year gap with a proof the world’s number theorists needed months to verify. As of Thursday it is true in a stricter sense: Anthropic announced that Claude has produced a complete, machine-checked formalization of the theorem in the Lean proof assistant — every inference compiled, nothing taken on faith. Thirteen million lines of Lean. Around 29,500 intermediate lemmas. Eleven days of largely autonomous work, at a cost of roughly six billion output tokens — between $60,000 and $300,000 at list prices, depending on whose invoice you read.
The route matters as much as the summit. Claude did not find a new proof; it rebuilt Wiles’s — the modular route through elliptic curves and Galois representations — in a formal language that permits no hand-waving. Every theorem a human mathematician had left informal, the model had to construct and verify before it could proceed. It is the first complete computer-checked verification of FLT, and it was completed before Kevin Buzzard’s own community formalization project, which had targeted 2029.
The machine did not out-mathematician Wiles. It out-patience everyone.
What a Proof Assistant Cannot Check
Buzzard’s reaction — the Imperial College mathematician behind Lean’s mathlib and the Xena project — was characteristically dry: “Anthropic has beaten me to it.” The community had assumed FLT formalization was a decade-scale grind requiring a thousand coordinated contributions. Instead, the bottleneck that took humans years — assembling the formal scaffolding beneath the summit — was absorbed by a model working in eleven days, failing, retrying, and re-deriving its way up the tower.
The caveats write themselves, and the announcement carries them honestly: this is verification, not discovery. No new mathematics came out of it; the creative act remains Wiles’s. But the economics are the story. A proof that consumed centuries of accumulated human craft is now reproducible as a bill — a five-figure render on someone’s API ledger. The demonstrable skill is not solving the unsolved; it is industrializing the already-solved. Every formal verification project in existence — cryptography, kernels, the Flyspeck catalogue — just repriced. The mathematicians who spent careers on formalization infrastructure are not obsolete this morning. They are, for the first time, outnumbered.
The Takeaways
- Anthropic announced September 4 that Claude completed a full Lean formalization of Fermat’s Last Theorem — the first complete machine-checked verification of Wiles’ 1995 proof.
- Scale: 13 million lines of Lean, ~29,500 intermediate theorems, 11 days of largely autonomous work, ~6 billion output tokens (≈$60k–$300k at list prices).
- The model rebuilt Wiles’ classical route (elliptic curves, Galois representations) rather than finding a new proof — verification, not discovery.
- Kevin Buzzard (Imperial College, Xena project): “Anthropic has beaten me to it” — the community formalization had targeted 2029.
- Every formal-verification effort — cryptography, kernels, Flyspeck — just repriced: industrializing the already-proven is now a billable render.
