In 1637, Fermat scribbled in a book margin that he had found a marvelous proof the margin was too small to contain. That note tormented mathematics for 358 years. In 1995, Andrew Wiles completed the proof, published across 129 pages in the *Annals of Mathematics*. On September 4, 2026, Anthropic announced that their internal model had fully formalized the theorem in Lean — in 11 days, across 60,474 files and over 13 million lines of code.
For scale: Wiles's printed proof is roughly the size of a brick. This artifact is a wall — full compilation on a 96-core, 512 GB machine takes 5 hours 52 minutes, nearly 20 times the compile time of mathlib, the Lean community's twenty-year mathematical library. Verifier Kevin Buzzard's own words: "It is a gigantic proof (over 13.4 million lines of code)".
Timeline: 389 Years of One Theorem
- 1637 — Fermat promises a marvelous proof in a margin
- 1993 — Wiles's three Cambridge lectures
- 1994 — A gap is found; Wiles and Taylor patch it over a year
- 1995 — Published in the Annals of Mathematics, 129 pages
- 2024 — Buzzard secures GBP 1 million to formalize FLT by hand
- 2026-08-07 — The machine starts running
- 2026-08-17 — At 10:00:57 PM, the FLT root node flips to PROVED
- 2026-09-04 — Repository published, blog post released
Who Did the Work
Officially: a "general internal research model, roughly comparable to Claude Fable 5.1," running dozens of agents on a multi-agent framework adapted from Claude Code, on the Prove2Me platform from Tianyi Peng's team at Columbia University. The paper is blunt — humans wrote no mathematics and no Lean, except the single line stating the target theorem. The machine logged its own note in the build: "Historic moment for this campaign."
The Verifier Was the Person Most Entitled to Grieve
Kevin Buzzard, professor at Imperial College, held a five-year, GBP 1 million EPSRC grant to lead the human community in formalizing FLT by hand. When Anthropic's email arrived, he was at the Green Man festival and dismissed it as crank mail. Three days later he saw the official announcement on a coffee shop's Instagram.
Then he did the right thing: downloaded the public repository, compiled it himself, and ran the Lean FRO comparator. His blog title concedes the race — *FLT: Anthropic has beaten me to it* — with the post's nail: "I've compiled the code base and run comparator on it — it checks out."
The trust chain has multiple layers. A second independent kernel, nanoda (~5,000 lines of Rust rewriting the Lean kernel), re-accepted all claims. The entire proof tree depends only on Lean's three standard axioms, with zero sorry. The comparator confirmed the proved statement matches a mathlib-only reference statement exactly — guarding against proposition-swapping. The sharpest HN objection was whether 13.4 million lines of agent code could exploit kernel loopholes (the Collatz incident earlier this year set a precedent). Buzzard's answer was unglamorous but solid: he line-by-line read the roughly hundred lines of code that weren't mathematical definitions or proofs — precisely to catch that kind of cheating.
The Route Follows Wiles's 1995 Path
The machine followed the early Darmon–Diamond–Taylor (1995) formulation, not a modern proof. The pipeline:
1. Assume a counterexample → Frey curve 2. Mazur's mod-p irreducibility 3. Langlands + Tunnell (handling p = 3) 4. The 3-to-5 switch 5. R = T modularity lifting 6. Ribet level-lowering to level 2 7. No cusp forms at level 2 → contradiction 8. FLT proved
Buzzard's verdict: "The formalization faithfully follows the early literature, adding nothing." The mathematics is Wiles's. The machine's contribution was translating 129 pages of human proof into machine-checkable form — and translating it wastefully.
On line counts: Anthropic says ~13 million (10.5 million after removing generated boilerplate), Buzzard counts 13.4 million, Claude self-reports 13.5 million — one repository, three figures. All point to the same thing: this wall is six mathlibs big.
Every Honest Asterisk
1. The machine only covered exponents p ≥ 17. Small primes were filled in by the human-led flt-regular project in 2025 — the smallest irregular prime is 37. Fine print: project author Brasca clarified that the regularity of 3, 5, 7, 11, and 13 was hand-proved in the repository, not cited off the shelf. 2. Intermediate theorems are bespoke. The paper itself admits the repository's "Ribet," "Wiles," and "Mazur" are special cases needed for the proof; the limitations document states they cannot be cited as general classical theorems. 3. Code quality falls short of mathlib standards: over 900 files exceed mathlib's 1,500-line cap, 31% of bytes are generated boilerplate, and two in five theorem statements are duplicate declarations. 4. The scoreboard hasn't updated. On Wiedijk's "Formalizing 100 Theorems" list — where FLT was the last entry — the official page still showed 99%, with FLT waiting in italics.
After the Wall Fell
Buzzard offered a deflating truth: "Mathematically, this work tells us almost nothing." He was already 99.9% sure FLT was true. The value lies in the infrastructure: autoformalization has gone from assistive tool to a pipeline capable of independently completing research-grade objects. His own project continues, this time following a modern route.
The cost comparison is amusing. Buzzard: GBP 1 million, five years. Anthropic: roughly 6 billion output tokens, 11 days — HN users estimated $100k–300k at API prices. Buzzard quipped: "I do suspect they spent more money..."
A quiet side experiment ran alongside: three consumer Claude Max subscriptions, three days, formalizing Vinogradov's three-primes theorem. Fermat's wall has fallen — and nobody has yet written the next list. I don't know the answer; I only know the question is much harder to avoid than it was last week.
References: Anthropic blog | Buzzard's verification post | Public repository | Wiedijk's list