Anthropic’s illustration for its research post on formalising Fermat’s Last Theorem. Credit: Anthropic A mathematician holds a five-year grant to formalise Fermat’s Last Theorem. It has been done for him in eleven days, and he says the result tells us nothing about mathematics. Anthropic published the proof on Friday.
Dozens of Claude agents wrote 13 million lines of Lean code and proved 30,300 intermediate theorems. They used 29,500 of those in a complete, computer-checked proof of a conjecture Pierre de Fermat scribbled in a margin around 1637. Kevin Buzzard of Imperial College London has led the community effort to formalise the same theorem since 2024, funded by the EPSRC. He compiled Anthropic’s code himself and ran the standard checking tool over it.
Then he wrote it up on his blog under the headline “Anthropic has beaten me to it”. What he actually said about it Buzzard’s verdict divides cleanly in two, and most coverage has taken only the first half. On the mathematics: it changes nothing. He puts the odds that Wiles’s proof is correct at 99.9%, and says most of the number theory community sits at 100%.
The formalisation, he wrote, “just faithfully follows the early literature on the proof and adds nothing”. On what it demonstrates, he is emphatic in the other direction. An AI swarm just formalised thousands of pages of literature end to end in eleven days. If that is now possible, he wrote, formalisation of modern research will start happening on the fly.
He added one line that no press release would carry. He was given £1m to run his project over five years. Anthropic took eleven days, and he wonders whether they spent more. The arithmetic on that wondering Anthropic says the run consumed about six billion output tokens.
They came from an internal research model it describes as roughly comparable to Claude Fable 5.1. Fable 5.1 costs $50 per million output tokens, the same price Anthropic set in September. Six billion output tokens at that rate is $300,000. That is an illustration rather than a cost.
The model was internal, so nobody raised an invoice, and a company’s own inference costs it less than list price. But it is the only public arithmetic available, and it sits against a £1m five-year grant. The first attempt failed Anthropic is unusually candid about this, and it is the most useful part of the post. The agents made early progress, then lost track of the project’s state and stopped collaborating.
Those failed runs still contributed around 7% of the non-boilerplate lines in the final proof. What fixed it was not a better model. It was Prove2Me, an open platform built by Anthropic researcher Tianyi Peng with collaborators at Columbia University. It maintains a graph of theorem statements, so agents can see what to attempt next.
It splits statements and proofs into separate files to speed compilation. And it keeps a plain-language description of each statement, so work can be found and reused. Add a multi-agent harness built on Claude Code and the same models finished the job in under a fortnight. We argued two days ago that the scaffolding around a model now decides what it achieves.
Here is the same lesson from the other direction, stated by the lab. Same agents, same weights, failure and then success, with a coordination platform as the only variable. Human input was two sentences Peng’s instructions to the swarm, as Anthropic reports them, ran to fragments. “Jacobian as a scheme sounds high priority.” “Push Mazur to be done soon.” The proof follows the 1995 exposition of the Wiles argument by Darmon, Diamond and Taylor. That is not the modern route Buzzard has been formalising.
It uses only Lean’s three standard axioms, and a comparator confirmed the theorem it proves matches the statement in Mathlib, the community’s mathematics library. At 13 million lines it is more than five times the size of Mathlib itself. Buzzard measured it at 13.4 million and says it takes nearly twenty times as long to compile, on a 96-core machine. He went looking for cheating Lean has had soundness bugs found in it recently, and a sufficiently determined agent could in principle exploit one to prove anything.
Buzzard checked. He asked an agent to flag every line of the repository that was not a definition or a proof. Roughly 100 lines came back, and he inspected them. They defined a convenience tactic.
He also reports that OpenAI’s models have reviewed Lean’s codebase and found no soundness issues in the version used. His own summary is that a hack finishing the job is extremely unlikely, and that the code is plainly developing the mathematics the proof needs. The bottleneck moved rather than vanished None of these 13 million lines can enter Mathlib as things stand. Buzzard, a Mathlib maintainer, says the library will not currently accept AI reviews.
Reviewers are also reluctant to review AI-generated code, because most AI-generated submissions are poor quality. The repository already has around 3,000 open pull requests, more than 600 of them active in the review queue. So the constraint has shifted from writing proofs to reading them. That is precisely the problem Anthropic says formalisation solves, arriving one layer up.
Buzzard also still has a job. His grant committed him to submitting foundational number theory to Mathlib, and to building a document that lets humans explore the modern proof. He doubts Anthropic will do the second. Where this sits against the rest of the year In August we reported Timothy Gowers arguing that the AI maths breakthroughs everyone quotes are counterexamples, not proofs.
A complete machine-checked proof is a different object, and it is the thing that argument said had not happened. It is also not new mathematics, which is the distinction Buzzard is pressing. OpenAI said in August that Astra had solved ten open problems. Claude found flaws in two cryptographic algorithms in July that expert review had missed.
Those were claims about discovery. This is a claim about verification, and verification is the easier half. One more number from the same post. Three researchers on personal Claude subscriptions formalised Vinogradov’s Three Primes Theorem in three days.
Buzzard heard about the FLT result late. He was at a music festival with poor reception. An email arrived from a stranger, titled “End-to-end Lean formalization of Fermat’s Last Theorem”, and he wrote the sender off as a crank.
