Claude Formalizes Fermat’s Last Theorem in 11 Days With Computer-Checked Proof
More than 350 years after Fermat’s Last Theorem became one of mathematics’ most famous problems, an AI system has taken on a different challenge surrounding the theorem: making its entire proof checkable by a computer.
Anthropic says Claude completed a formalized version of the theorem’s proof in 11 days, producing about 13 million lines of Lean code and proving roughly 29,500 intermediate theorems along the way. The finished work was checked using Lean, a programming language and proof assistant designed to verify mathematical reasoning step by step. The achievement does not mean Claude discovered a new proof of Fermat’s Last Theorem. The theorem was already proved by mathematician Andrew Wiles in 1995. What changes here is how that proof can be checked: instead of relying entirely on mathematicians to examine thousands of connected mathematical steps, the formalized version allows a computer to verify the logical structure.
Turning a 1995 proof into something a computer can check
Fermat’s Last Theorem states that there are no positive integers that satisfy the equation aⁿ + bⁿ = cⁿ when n is greater than 2.
Pierre de Fermat wrote the claim in the margin of a book around 1637, famously suggesting that he had found a proof but that the margin was too small to contain it. It would take more than three centuries before a complete proof was established. Wiles presented his proof in 1993, but a gap was discovered during the verification process. He spent another year repairing the problem with Richard Taylor before the final proof was published in 1995. The proof relied on mathematical ideas that were far beyond anything available in Fermat’s time.
Formalizing that proof is a different task. A human mathematician can leave out steps that seem obvious to another expert. A proof assistant cannot. Every logical connection has to be expressed in a form the computer can check. That is why formalizing Fermat’s Last Theorem was expected to take years. The blueprint used by mathematicians for the initial part of the formalization alone runs to 86 pages.
Claude worked through thousands of mathematical steps
Claude approached the problem through a system in which multiple AI agents could work on different parts of the formalization.
The agents had to define mathematical concepts, prove intermediate results and then use those results to tackle increasingly difficult parts of the overall proof. An earlier set of attempts struggled because the agents lost track of the project and failed to coordinate effectively.
The process improved after the team moved the work to Prove2Me, a collaborative platform designed for mathematical formalization. The platform maintained a structured map of the relationships between theorem statements, allowing different agents to work in parallel while keeping track of which results depended on others.
By the end, Claude had produced computer-verifiable proofs for about 30,300 theorems during the project, with around 29,500 ultimately forming part of the final proof. The resulting 13 million lines of Lean code are more than five times the size of Mathlib, the major community library of formalized mathematics that the work builds upon.
Why formalized mathematics matters
The significance of the project goes beyond one famous theorem. Mathematical proofs can become extremely long and complicated. Checking a new result may take months or even years, particularly when it depends on many earlier results. A formal proof gives mathematicians another way to establish that each step follows from the ones before it.
That could become increasingly useful as AI systems begin producing more mathematical work. If an AI proposes a complicated proof, converting it into a language such as Lean could provide a much stronger way to check whether the argument actually holds. It also opens the possibility of systematically formalizing older mathematical literature. Large parts of mathematics remain understandable to humans but are not yet represented in a form that computers can automatically verify.
AI is moving deeper into mathematical research
The Fermat project also shows how the role of AI in mathematics is changing. The headline achievement is not that Claude replaced Wiles or discovered the theorem. Instead, it handled an enormous amount of the painstaking work required to translate existing mathematical reasoning into a machine-checkable form. Anthropic says the completed proof uses only Lean’s three standard axioms, with no unproved placeholders left in the final result. The full formalization has also been made available for further examination.
For mathematicians, that could prove useful as AI-generated mathematics becomes more common. Instead of asking humans to manually inspect every detail of increasingly complex AI-generated arguments, formal verification could provide an additional layer of confidence. Fermat’s Last Theorem took centuries to solve and decades more to turn into a form suitable for computer verification. The latest achievement suggests that the next chapter of mathematical research may involve not just asking AI to find answers, but also using AI to make those answers easier for machines — and eventually humans — to check.
