In 1637, Fermat wrote in a book margin that he had found a marvelous proof the margin was too narrow to contain. The statement 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 an internal model had fully formalized the theorem in Lean — in 11 days, producing 60,474 files and more than thirteen million lines of code.
To put the scale in perspective: Wiles's proof prints out roughly the size of a brick. This artifact is a wall: a 96-core machine with 512 GB of RAM needs 5 hours 52 minutes for a full compile — nearly 20 times the compile time of mathlib, the Lean mathematical library the global community has built over two decades. Kevin Buzzard, who verified it, put it plainly: "It is a gigantic proof (over 13.4 million lines of code)".
Who actually did the work
The official account: a "general internal research model, roughly on par with Claude Fable 5.1," running dozens of agents in a multi-agent framework adapted from Claude Code, on the Prove2Me platform of Tianyi Peng's team at Columbia University. The paper is blunter — humans wrote no mathematics and no Lean, except the single line stating the target theorem. The run started August 7; at 10:00:57 PM on August 17, the FLT root node flipped to PROVED. The machine logged the moment itself: "Historic moment for this campaign."
The verifier: the person most entitled to be upset
Kevin Buzzard, professor at Imperial College, holds a £1 million, five-year EPSRC grant to formalize FLT with a human community. 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 Instagram, at a café in London.
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" — and the body carries the definitive line: "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 (about 5,000 lines of Rust reimplementing the Lean kernel), accepted all claims; the entire proof tree depends only on Lean's three standard axioms with zero sorrys; and the comparator confirmed the proved proposition exactly matches a reference statement importing only mathlib — guarding against statement-swapping. The sharpest HN objection was whether 13.4 million lines of agent code could exploit kernel loopholes (the Collatz incident earlier this year showed such precedent). Buzzard's answer was laborious but solid: he read, line by line, the roughly hundred lines that are not mathematical definitions or proofs.
The route taken: the 1995 path
The machine followed the early Darmon–Diamond–Taylor 1995 formulation, not the modern proof. Buzzard noted the key point: "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 — a spectacularly wasteful translation.
On size, three counts disagree slightly: Anthropic says 13 million lines (10.5 million excluding generated boilerplate), Buzzard counted 13.4 million, Claude self-assessed 13.5 million. All point to the same thing: this wall is roughly six mathlibs large.
The honest asterisks
- Only p ≥ 17 was machine-proved. Small exponents were filled in by the human flt-regular project in 2025 — the smallest non-regular prime is 37. Its author, Brasca, clarified that regularity for 3, 5, 7, 11, 13 was proved by hand inside the repository, not cited from existing results.
- Intermediate theorems are bespoke. The paper itself admits the repository's "Ribet," "Wiles," and "Mazur" results are special cases needed for the proof; the limitations document says they cannot be cited as general classical theorems.
- Code quality falls short of mathlib: over 900 files exceed mathlib's 1500-line limit, 31% of bytes are generated boilerplate, and two-fifths of theorem statements are duplicates.
- The scoreboard hasn't updated: Wiedijk's "Formalizing 100 Theorems" list — where FLT is the final item — still sits at 99%, with FLT waiting in italics.
After the wall falls
Buzzard offered a deflating truth: "mathematically this tells us almost nothing." He was already 99.9% sure FLT was true. The value is infrastructure: autoformalization has gone from auxiliary tool to a pipeline capable of completing research-grade objects. His own project continues, now on the modern route.
The cost comparison is amusing: Buzzard — £1 million, five years. Anthropic — roughly 6 billion output tokens in 11 days; HN users estimated $100k–$300k at API prices. Buzzard joked: "I do suspect they spent more…"
A quieter side experiment ran alongside: three consumer Claude Max subscriptions formalized Vinogradov's three-primes theorem in three days. Fermat's wall has fallen; nobody has yet written the next list of what should be formalized. I don't know the answer — only that the question has become much harder to avoid than last week.
References: Anthropic blog | Buzzard's verification post | Public repository | Wiedijk's list