Anthropic says it has reached a historic milestone in AI-assisted mathematics: Claude produced a complete, computer-verifiable formalization of Fermat’s Last Theorem. The work took 11 days and generated around 13 million lines of code in Lean, a language designed to express and check mathematical proofs.
The news does not mean that Claude discovered a new theorem. Its achievement lies in turning an extremely complex mathematical proof into a structure that a proof assistant can review step by step. Why does that matter so much? Because verifying a proof can take months or years when it depends solely on other mathematicians’ careful reading.
What Fermat’s Last Theorem proves
Fermat’s Last Theorem states that there are no positive integers a, b, and c that satisfy:
aⁿ + bⁿ = cⁿ
for any integer exponent n > 2.
Pierre de Fermat wrote this statement around 1637 in the margin of a book and added that he had found an extraordinary proof, but that the margin was too small to contain it. The supposed proof never appeared, and for more than three centuries, generations of mathematicians tried to solve the problem.
The first accepted proof arrived in 1995, when Andrew Wiles published a proof based on advanced number theory tools. The work, developed together with Richard Taylor after they corrected a critical issue, ran to 129 pages and connected areas such as elliptic curves, modular forms, and algebraic geometry.
From a human proof to a verifiable proof
A proof written for people usually leaves out steps considered obvious. A mathematician can say that a consequence follows easily from an earlier result and continue with the argument. Lean, by contrast, needs to receive every logical connection explicitly.
Lean is a proof assistant. It does not try to understand a proof the way a human reader would. Instead, it checks that each statement follows correctly from definitions, previous theorems, and accepted axioms. If a step is missing or a rule is applied incorrectly, the system rejects the proof.
Formalizing a proof does not replace mathematical explanation for humans, but it offers an extremely rigorous way to check its logical structure.
The challenge is translating decades of mathematical knowledge into a format that a computer can process. For Fermat’s Last Theorem, the community expected that process to take years. The initial outline used by the formalization project developed at Imperial College London alone ran to 86 pages.
How Claude and the AI agents worked
According to Anthropic, Claude worked with dozens of agents coordinated through Prove2Me, a collaborative platform for formalizing mathematics developed by Tianyi Peng and his colleagues at Columbia University.
The agents divided up tasks such as defining concepts, proving intermediate results, and connecting those results to increasingly complex statements. In total, they produced verifiable proofs for 30,300 theorems, 29,500 of which were used in the final proof.
The system consumed approximately six billion output tokens from an internal research model described by Anthropic as comparable to Claude Fable 5.1. The final proof is more than five times the size of Mathlib, the main library of mathematical results on which this work is based.
The process was not successful from the start. The first attempts lost the project state, and the agents stopped collaborating effectively. Those failed efforts contributed around 7% of the non-repetitive lines in the final version, showing that agent autonomy still depends heavily on how the work environment is organized.
What this advance really contributes
The novel part is not a new proof of the theorem. Claude followed a simplified version of Wiles’s strategy, based on the work of Henri Darmon, Fred Diamond, and Richard Taylor, while also relying on previous formalizations from other mathematical projects.
What is new is the speed and scope of the automated verification. Anthropic says that Lean checked the proof using only its three standard axioms, and that a comparator confirmed that the statement used matches the formulation of Fermat’s Last Theorem available in Mathlib.
Kevin Buzzard, a mathematician at Imperial College London and one of the people behind the community Fermat formalization project, reviewed the result and said that the work represents an important step toward the automatic formalization of large parts of the mathematical literature.
This could change academic review. When an AI produces a proof, a human researcher still needs to understand the strategy, assess its relevance, and check that the result answers the right question. But a formalized proof can handle one particularly demanding part: verifying that the logical chain contains no errors.
The difference between discovering and verifying
In recent years, some AI systems have attempted to produce new mathematical results, such as advances related to the Riemann hypothesis. Formalizing Fermat’s Last Theorem belongs to a different category.
Here, the AI is not presenting an original mathematical idea. It is carrying out a task comparable to checking a calculation with a calculator, although on a vastly larger scale. The proof must be expressed in a formal language and pass the system’s checks.
That does not make mathematicians unnecessary. Formalization still requires human decisions about which strategy to follow, which libraries to use, and how to divide up the problem. In this case, Tianyi Peng provided high-level instructions, such as prioritizing the construction of a Jacobian as a scheme or moving forward with Mazur’s theorem.
The difference is that a considerable part of the work involved in translating, searching for lemmas, and connecting results could be delegated to AI agents. Could this workflow become a common research tool? Anthropic believes it could.
Toward mathematics that is easier to audit
The team also reports a smaller experiment: three personal Claude Max subscriptions were used to formalize applications of the Hardy–Littlewood circle method. The agents collaborated on Prove2Me and completed the formalization of Vinogradov’s three-primes theorem in three days.
These results point to a possible evolution in mathematical work. Instead of publishing only an explanation in natural language, researchers could also provide a formalized version that anyone can check again with the appropriate tools.
Formalization could help detect old errors in the mathematical corpus, reduce the burden on reviewers, and make it easier to assess proofs generated by language models with confidence. It also appears to function as a self-checking tool for AI itself: when trying to express every step in Lean, the model is forced to check whether its assumptions really lead to the result.
Even so, important limitations remain. A formal proof can confirm that a conclusion follows from its premises and axioms, but it cannot by itself decide whether the chosen problem was interesting, whether the strategy is understandable, or whether a definition correctly reflects the researcher’s original intention.
The story of Fermat’s Last Theorem began with a note in the margin of a book and ended up connecting mathematics developed over centuries with millions of lines of code. Claude’s achievement does not erase that human history. It turns it into a new kind of object: a proof that can not only be read, but also executed and audited step by step.
Original source
https://www.anthropic.com/research/formalizing-fermats-last-theorem