Anthropic said on Sept. 4, 2026, that teams of Claude AI agents, working largely on their own, produced the first complete, computer-checked proof of Fermat's Last Theorem in about 11 days. They wrote the proof in Lean, a programming language whose software checks every step of a proof the way a calculator checks a sum. It is a machine check of a famous proof that mathematicians already had, not a new solution of the theorem.
Anthropic said the work ran on Prove2Me, an open platform designed by Tianyi Peng and colleagues at Columbia University for formalization, the rewriting of math into a form a computer can check. The finished proof, Anthropic said, contains about 13 million lines of Lean and proves roughly 29,500 smaller theorems that the final proof builds on. The agents ran on an internal general-purpose research model that Anthropic described as roughly comparable to Claude Fable 5.1, and it wrote about six billion small chunks of text, often parts of words, along the way.
Anthropic said early attempts with several agents stalled when the agents lost track of where the project stood. Prove2Me's map of how the theorems depend on one another, separate files for each statement and its proof, and a search tool that finds theorems from plain-language descriptions let the agents work in parallel, the company said. It says the proof relies only on Lean's three standard axioms, its basic starting assumptions, and that a checking tool confirmed the theorem it proves matches the statement of Fermat's Last Theorem in Mathlib, Lean's shared math library. Human input on the math, Anthropic says, was limited to occasional high-level steering from Peng.
Anthropic says the proof follows a simplified account of the Wiles-Taylor-Wiles proof by the mathematicians Darmon, Diamond and Taylor. Anthropic contrasts the project with AI work that claims new mathematics: what is new here, it says, is the checking of an existing proof.
Kevin Buzzard, a mathematician at Imperial College London, compiled the code and ran the checking tool himself, writing on his blog the same day that it checks out. He congratulated the team on the milestone and stressed that the work adds essentially no new mathematics. He noted that it follows the Darmon-Diamond-Taylor route rather than the modern proof he is formalizing, and said his project funded by the Engineering and Physical Sciences Research Council (EPSRC) still aims at contributions to Mathlib and at tools that let people read and explore the math, which Anthropic's release does not replace. In a Sept. 7 news report, Buzzard said that two years earlier such a formalization would have been a fantasy. Rutgers number theorist Alex Kontorovich said in the same report that the 13-million-line computer-checked proof "just completely blew my mind."
It is not yet clear how much of the 13-million-line proof can be reworked into lasting contributions to Mathlib, how reviewers will guard against rare flaws in Lean's own checking at this scale, or whether the same approach can keep pace with new research rather than a settled 1990s proof. The counts of lines and text come from Anthropic.