Fermat’s claim sat unproven for more than 350 years. Andrew Wiles delivered the proof in 1995, 129 pages of it, and mathematicians needed months to check it. Since 2024, Kevin Buzzard and a team at Imperial College have been working to formalize that proof in Lean, meaning rewriting it so a computer can verify every step. Expected duration: years. On September 4, Anthropic announced that Claude did it in eleven days.
What happened
Tianyi Peng, an Anthropic researcher who also runs a group at Columbia University, wanted to see how far Claude could get with formalizing Fermat’s Last Theorem. The answer: all the way. A complete proof, checked by Lean. 13 million lines of Lean code, 29,500 intermediate theorems, roughly six billion output tokens. The proof is five times the size of Mathlib, the entire community library of formalized mathematics it builds on.
Dozens of Claude agents worked in parallel, coordinated by a multi-agent harness built on Claude Code. The model was an internal research model, which Anthropic describes as roughly comparable to Fable 5.1. Human input was limited to occasional nudges from Peng about which subarea should get priority next.
The first attempt failed. The agents lost track of where the project stood and stopped collaborating in any useful way. About 7 percent of the lines in the final proof still come from those failed runs. What made it work was Prove2Me, an open platform from Peng’s group. It maintains a dependency graph of theorem statements, and agents pull their next task from it. Statements and proofs live in separate files, which speeds up Lean compilation, and every theorem carries a natural-language description so agents can find what has already been proven.
On August 18 at 02:00 UTC, the root of the graph flipped to PROVED. Anthropic published excerpts from Claude’s reasoning as it noticed: Historic moment, modulo re-check.
What Kevin Buzzard says
Buzzard is the person who just got beaten to the finish line, and he reviewed the proof. He compiled the code, ran the comparator to confirm that the proven statement matches Mathlib’s own definition of Fermat’s Last Theorem, and wrote on his blog: it checks out. The proof uses only Lean’s three standard axioms. Compiling takes nearly 20 times as long as Mathlib, on a machine with 96 cores.
His post is titled “FLT: Anthropic has beaten me to it,” and he sounds remarkably relaxed about it. Mathematically, he says, the proof teaches us nothing new. The field was already 100 percent sure Wiles was right. What it does show is what autoformalization can do now. If thousands of pages of literature can be checked end to end in eleven days, research will soon be formalized as it happens, and machines will flag every gap that used to be papered over with “known to the experts.” That is the part he finds exciting.
His project continues regardless. He promised the EPSRC he would get the building blocks of modern number theory into Mathlib and build a document that lets humans explore the proof. Anthropic did neither. And Claude did not formalize the modern proof but the 1995 Darmon-Diamond-Taylor exposition, with a few shortcuts that only work for primes from 37 upward. The smaller ones were already formalized.
One number from his post sticks: he received one million pounds for five years. In the comments, someone works out that six billion output tokens at API prices come to about 300,000 dollars.
Why this is more than a math anecdote
For me the real story is the pattern underneath. A swarm of agents, a shared task graph, a compiler as an incorruptible referee, and suddenly a multi-year project becomes a two-week project. Anthropic tried the same thing at a smaller scale: three researchers with three ordinary Claude Max subscriptions used Prove2Me to formalize Vinogradov’s three primes theorem in three days.
The full proof is on GitHub, along with a written walkthrough of its structure. If you know Lean, go look. If you don’t, remember this: the argument that “you can’t verify AI-generated math” just got a large hole in it. Verification is exactly what formalization is for.
Sources: Anthropic: Formalizing Fermat’s Last Theorem, GitHub: anthropics/fermats-last-theorem, Kevin Buzzard: FLT: Anthropic has beaten me to it, SiliconANGLE: Anthropic uses Claude to formalize proof of Fermat’s Last Theorem, Hacker News discussion