Claude Formalized Fermat's Last Theorem in 11 Days

Did an AI just prove Fermat's Last Theorem? No. Andrew Wiles did that in 1995. What Anthropic announced on September 4 is something else, and arguably more useful: Claude translated Wiles's proof into Lean 4 code that a computer can check line by line. Mathematicians call this formalization, and for this particular theorem they expected it to take years.

What was actually done

Per Anthropic's research post, the work was carried out by an internal research model "roughly comparable to Claude Fable 5.1." Over 11 days it produced 13 million lines of Lean and proved 30,300 intermediate theorems, 29,500 of which made it into the final proof. The result compiles, meaning every step was mechanically verified. Kevin Buzzard of Imperial College London reviewed it, and a separate check confirmed the theorem statement matches the version in the Mathlib library.

Buzzard's assessment is measured but clear: "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature."

What "11 days" leaves out

The calendar time is not one agent working straight through. Several dozen agents ran in parallel and generated 6 billion output tokens between them. Anthropic did not publish the cost; a rough estimate lands well above a small company's annual software budget.

The first attempt failed. The run succeeded only after the team added Prove2Me, an open-source tool built by Tianyi Peng's group at Columbia that maintains the dependency graph between theorems and decides which piece agents attack next. By Anthropic's own count, about 7% of the non-boilerplate lines are leftovers from failed attempts, and the 13-million-line proof is "likely much longer than it needs to be."

There is also a foundation. The project builds on Buzzard's multi-year Imperial FLT effort and on flt-regular, an existing Lean formalization of Kummer's theorem. Nobody started from zero; without the groundwork laid by humans, this result does not exist.

Why it matters anyway

Because until now, most "AI does math" headlines described text a human still had to check. In a formalized proof, the compiler does the checking, and the model's chance of writing something persuasive but wrong drops to nil. That is a tool capable of catching errors peer review missed for years, and Anthropic names that as the goal: reduce the review burden and flush mistakes out of the literature.

The skeptic in us adds one thing. A 13-million-line proof is not something a person reads to learn from. We know it is correct; understanding why is still left to humans.

For readers who are not mathematicians

Nobody is renting agents to formalize Fermat. But the same loop, model generates, a strict verifier checks, failures get discarded, works in any job with a hard checker: code that must type-check, rewrites that must pass tests, data transformations that must fit a schema. A software team can rewrite a legacy module this way today without spending 6 billion tokens, because the rule is the same at every scale: the stricter the verifier, the more you can trust the agent. Where no such checker exists, this result offers you no guarantee at all.

Sources: Anthropic: Formalizing Fermat's Last Theorem, GitHub: proof repository, SiliconANGLE