Tech & Science Desk
At 10:00:57 p.m. on August 17, a computer program that had been grinding away autonomously for a week and a half stopped, looked at what it had done, and typed three checkered-flag emojis.
"The FLT root reads PROVED," it wrote. "Historic moment for this campaign."
Then, in an earlier note that delighted every mathematician who read it, the same system hedged with the most human caveat imaginable: "Historic moment (modulo re-check)."
The re-check held. On September 4, Anthropic published what it says is the first complete, computer-verified proof of Fermat's Last Theorem — the most famous unsolved problem in mathematics until Andrew Wiles cracked it in 1995. Claude, Anthropic's AI model, did it in eleven days. Along the way it wrote 13 million lines of code and proved 29,500 separate intermediate theorems.
It is, by a wide margin, the largest formal mathematical proof ever constructed — and it has landed like a grenade in a discipline that spent three thousand years insisting certainty is something only humans can confer.
WHAT FERMAT ACTUALLY WROTE
Around 1637, Pierre de Fermat — a lawyer by trade, a mathematician by obsession — was reading his copy of Diophantus's Arithmetica when he jotted a claim. No three positive whole numbers a, b and c, he wrote, can satisfy aⁿ + bⁿ = cⁿ for any n greater than 2.
For n equals 2, the solutions are everywhere: 3, 4, 5. But cubes? Fourth powers? Fermat said no. Never. Not once, in the infinite sprawl of integers.
And then he added the sentence that has tormented mathematics ever since: "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain."
He never wrote it down elsewhere. He died in 1665. For the next three and a half centuries, some of the finest minds who ever lived threw themselves at a one-line conjecture — and bounced off it.
In 1908, a prize of 100,000 gold marks was announced for a correct proof. In the first year alone, 621 incorrect attempts poured in — not cranks with envelopes, but formally submitted, formally rejected proofs.
THE MAN WHO ALMOST LOST IT
Then came Andrew Wiles. In June 1993, the British mathematician stood up at Cambridge and delivered three lectures building toward a conclusion he had worked on in near-secrecy for seven years. At the end, he wrote Fermat's Last Theorem on the board and sat down. The room went briefly insane.
Two months into the verification effort, a reviewer asked Wiles a question he could not answer. There was a genuine hole in the load-bearing wall of a 200-page argument.
Wiles spent the next year trying to fill it, nearly abandoning the whole thing, until he realised that an approach he had discarded years earlier could be welded onto the approach that had failed. Together, they worked.
The corrected proof was published in May 1995. It ran to 129 pages and relied on machinery — modular forms, elliptic curves, Galois representations — unintelligible not just to Fermat but to every mathematician before the twentieth century.
WHY "PROVED" WASN'T ENOUGH
A published proof is not the same as a certain proof. Wiles's argument took specialists months to check — and they still missed the gap on the first pass. Thomas Hales's 1998 proof of the Kepler conjecture spent four years in review before a twelve-referee panel gave up and settled for "99% certain." Grigori Perelman's proof of the Poincaré conjecture took four years and three separate 300-page expositions to accept. And occasionally, results that are flat wrong are accepted for years while others build theories on top of the rot.
The proposed fix is formalisation: rewriting a proof in a language so unforgiving that a computer can check every logical step automatically, from the bare axioms upward. The tool of choice today is Lean, a proof assistant with a community library called Mathlib built by hundreds of volunteer mathematicians.
The catch is brutal. A human proof skips the obvious steps — that's what makes it readable. Lean permits no skipping. Every triviality must be spelled out.
In 2024, Kevin Buzzard of Imperial College London kicked off a multi-year project to formalise Fermat in Lean. The realistic timeline everyone assumed was years. Possibly a decade.
ELEVEN DAYS
Tianyi Peng, an Anthropic researcher, set out to test whether Claude could make any progress at all. The first attempts failed outright — the machine equivalent of a research group where nobody reads anyone else's email.
The breakthrough came with Prove2Me, an open collaborative platform that maintains a live map of what has been proved, what is being attempted, and what is blocked, so dozens of Claude agents could work in parallel without tripping over one another.
With that scaffolding, a swarm of agents completed the job in under two weeks, burning roughly six billion output tokens.
The numbers are staggering: 13 million lines of Lean. 30,300 theorems proved, 29,500 used in the final chain. The finished artefact is more than five times the size of Mathlib itself. Lean's kernel checked the whole thing using only its three standard axioms. A separate comparator confirmed that Claude proved exactly what it claimed to prove — no sneaky redefinitions.
Human input was limited to occasional high-level nudges. Two of them, preserved in the write-up, are almost comically terse: "Jacobian as a scheme sounds high priority." "Push Mazur to be done soon."
THE VERDICT FROM IMPERIAL
Anthropic sent the proof to Kevin Buzzard — the man whose multi-year project it had just leapfrogged.
His response was not what cynics predicted.
"This extraordinary autoformalization achievement proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics," Buzzard said. "Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon."
He went further: "If automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of modern mathematical literature. Such techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees."
THE FINE PRINT
Before anyone declares mathematicians obsolete, several things need saying.
First: Claude did not discover anything. The proof Claude formalised is a simplified version of Wiles's argument laid out by Darmon, Diamond and Taylor. Every genuinely hard idea belongs to humans.
Second: it did not start from nothing. The formalisation adapts pieces from Buzzard's project and sits on Mathlib — years of volunteer labour.
Third: 13 million lines is not a flex, it's a confession. Anthropic concedes the proof is "likely much longer than it needs to be." A human formaliser would have written something shorter and more beautiful. Claude wrote something enormous and correct. Those are different virtues.
THE THREE-DAY THEOREM
The detail with the longest tail may be a throwaway line near the end. Some Anthropic researchers ran a small side experiment using three ordinary personal Claude Max plans — the kind any member of the public can buy — and their agents jointly formalised Vinogradov's Three Primes Theorem in three days.
That is a serious result in analytic number theory, formalised on consumer subscriptions over a long weekend. If that generalises, the bottleneck on formal mathematics stops being compute and starts being imagination.
WHAT THIS MEANS
You are probably not going to formalise a theorem this year. But you already live downstream of mathematics you cannot check — in the encryption protecting your bank login, in the error-correcting codes keeping your video call from dissolving.
The trustworthiness of that foundation currently depends on a small number of overworked specialists reading each other's work carefully — and occasionally missing things for years. If autoformalisation scales, that changes: results get machine-checked as routine, and errors get caught in weeks rather than decades.
AI systems have begun producing purported mathematical results faster than humans can verify them. A flood of machine-generated proofs that only humans can check is a bottleneck. A flood that machines can check is an industry.
Anthropic's framing is telling: formalisation is a place it feels "unambiguously good" about AI's role. Verification, unlike creation, doesn't take anything away from anyone. It just makes it harder to be wrong.
THE MARGIN, REVISITED
There is a joke doing the rounds among mathematicians this week, and it is a good one.
Fermat said his marvelous proof wouldn't fit in the margin. Three hundred and eighty-nine years later, the definitive machine-checked version doesn't fit in anything smaller than 13 million lines of code.
He was right about one thing, at least. The margin really was too small.
Whether he was right about having a proof at all remains, as it has always been, the one part nobody can check.
