Claude produced a computer-checked proof of Fermat's Last Theorem in Lean in 11 days
The model translated an existing proof into a formal proof assistant rather than discovering new mathematics. That distinction is the whole story, and it is a bigger result than it sounds.
Anthropic says Claude has produced a fully computer-checked formalisation of Fermat's Last Theorem in Lean, translating an existing proof into the proof assistant over 11 days. The company announced the result on 4 September.
The distinction between this and "an AI proved Fermat's Last Theorem" is the entire content of the story. Andrew Wiles proved the theorem in 1994. What Claude did was render that proof — and the enormous body of mathematics it depends on — into a formal language where every step is mechanically verified by a computer.
That is a smaller claim about mathematical creativity and a much larger one about sustained, verifiable machine work than the headline suggests.
Why formalisation is hard
A published mathematical proof is written for other mathematicians. It compresses. It says "similarly" and "it is easy to see" and "by a standard argument," leaving steps that a competent reader can reconstruct. A proof assistant cannot reconstruct anything: every one of those elisions has to be expanded into complete formal detail before Lean accepts it.
The Fermat formalisation effort has been running for years as a human project under Kevin Buzzard at Imperial College London, precisely because the theorem sits on top of a tower of modern number theory — modular forms, Galois representations, elliptic curves — most of which had to be formalised first before the top of the tower could be attempted.
Eleven days against that backdrop is the figure worth attention.
What makes it different from a benchmark
Almost every claim about AI mathematical ability suffers the same weakness: the grader is a human or another model, and the result is a judgement. Formalisation has no such problem. Lean either accepts the proof or it does not. There is no partial credit, no plausible-sounding error, no hallucination that survives review, because the reviewer is a type checker.
This makes it one of the few tasks where a long-horizon agentic claim can be fully verified from outside. If the Lean files compile, the work is correct. That is a stronger form of evidence than any benchmark score released this year.
It is also a task shaped exactly to a model's strengths: enormous, tedious, highly structured, with immediate mechanical feedback on every attempt. Formalisation is the kind of labour that has bottlenecked mathematics because it is unrewarding for humans to do, not because it is conceptually deep.
What has not been established
Anthropic has not said how much compute the 11 days consumed, how much human direction was involved in decomposing the task, how much of the supporting library Claude built versus reused from existing formalisation work, or whether the output has been independently reviewed by the Lean community.
That last point matters most. The mathematical community's standard for such results is review by the maintainers of the relevant libraries, and that review has not yet happened publicly.
The result also arrives days before a considerably less flattering mathematical story: NYU's Tristan Buckmaster accusing OpenAI of racing him to a Millennium Prize problem after learning of his progress. Formalising a known proof and claiming a novel one are different acts, and the industry is currently conflating them.
Runs the newsroom. Rename this profile in the studio to your own byline.
Related
Every weekday, the AI stories that moved money or shipped code.
No cross-posting, unsubscribe anytime. See all newsletters