Claude does not solve Fermat: he makes his proof verifiable by Lean

Anthropic publishes the first complete formalization of Fermat's Last Theorem, produced in eleven days by several Claude agents and verified with the Lean proof assistant.

Claude did not discover a new proof of Fermat’s Last Theorem. Instead, Anthropic’s model translated the existing mathematical argument into Lean, a language in which every logical step can be checked by a computer. The distinction matters: the result does not change what mathematicians know about the theorem, but it could transform how they verify increasingly long and complex proofs.

Fermat’s Last Theorem states that no positive integers aa, bb, and cc satisfy an+bn=cna^n+b^n=c^n when nn is greater than 2. Pierre de Fermat wrote the claim around 1637, adding that he had found a proof too large to fit in the margin. More than three centuries passed before Andrew Wiles presented a successful approach in 1993.

That first version contained a serious gap. Wiles spent about a year repairing it with Richard Taylor before publishing the completed proof in 1995. The argument relied on sophisticated results from number theory and ran to more than a hundred pages. Checking it required several specialists and months of work.

Formalization addresses a different problem. A conventional mathematical paper is written for experts and leaves out steps that its readers are expected to infer. A proof assistant requires every definition, implication, and dependency to be made explicit. Once the formal version compiles, the software verifies that the conclusion follows from the stated axioms and previously established results.

This approach provides a stronger form of verification, but producing the formal proof has traditionally demanded considerable human labor. The available libraries contain only part of the mathematical knowledge used in published research. Formalizers must therefore encode not only the main argument, but also many intermediate concepts and apparently routine results.

In 2024, mathematician Kevin Buzzard launched a community project to formalize Fermat’s Last Theorem with Lean. The work was expected to take several years. It built on Mathlib, Lean’s main mathematical library, as well as a separate project covering cases involving regular primes.

Anthropic researcher Tianyi Peng later tested whether Claude could accelerate the effort. According to the company, dozens of agents working largely autonomously completed an end-to-end formalization in eleven days. They generated approximately 13 million lines of Lean, proved about 30,300 intermediate theorems, and used 29,511 of them in the final dependency graph.

The scale of those figures should be interpreted carefully. The repository is more than five times the size of Mathlib by line count, but that does not mean it contains five times as much mathematical knowledge. Mathlib is extensively reviewed and optimized, whereas the generated code contains duplication, long proofs, support files, and unsuccessful work that could probably be reduced substantially.

The agents produced roughly 533,000 local lemmas during the project. Only part of that material was ultimately needed. Anthropic estimates that failed early attempts still account for around 7% of the non-boilerplate code retained in the final repository.

The mathematical route is not new. Claude followed a simplified exposition of the Wiles proof developed by Henri Darmon, Fred Diamond, and Richard Taylor. Broadly speaking, the argument connects Fermat’s equation to elliptic curves and modular forms. Results showing that certain curves must be modular then lead to the contradiction required to prove the theorem.

The Anthropic formalization handles the main case for prime exponents of at least 17 and combines it with results already available in the `flt-regular` project. The smaller exponents and other reductions needed to reach the standard statement are supplied through these existing formal developments.

This dependence does not diminish the technical work, but it places it in context. Claude did not start with only the axioms of mathematics and rediscover every theory required by Wiles. It relied on Mathlib, previous Lean projects, existing theorem statements, and more than a hundred files adapted from the Imperial College London initiative.

Human guidance was limited but not absent. Peng provided occasional high-level priorities, such as asking the agents to focus on Jacobians or to complete a theorem associated with Barry Mazur. Humans also selected the mathematical route, supplied the infrastructure, incorporated earlier formal work, and checked the finished repository.

The first attempts did not succeed. Agents initially made progress independently, then lost track of the project’s overall state and stopped coordinating effectively. A long formal proof creates a management problem: thousands of dependent statements must be assigned, proved, reused, and updated without different workers duplicating or contradicting one another.

The decisive change came from Prove2Me, an open collaborative platform developed by Peng and researchers at Columbia University. It represents the proof as a directed acyclic graph in which each node corresponds to a theorem and the links record its dependencies.

This graph gave the agents a shared view of the work. They could identify statements whose prerequisites were already available, select the next proof to attempt, and add successful results for other agents to reuse. The structure also reduced the effects of limited context and memory degradation during a project lasting several days.

Prove2Me separates theorem statements from their proofs. This arrangement speeds up compilation and allows dependencies to remain stable even while the implementation of an individual proof changes. Natural-language descriptions attached to the statements also make it easier to search for an existing result before creating another version.

Anthropic combined this platform with a multi-agent system based on Claude Code. The complete run consumed approximately six billion output tokens from an internal general-purpose research model described as roughly comparable to Claude Fable 5.1.