The Pulse
Claude Turns Wiles’s Fermat Proof Into 13 Million Lines of Lean
Anthropic says Claude produced the first complete computer-checked formalization of Fermat’s Last Theorem in 11 days. The system generated 13 million lines of Lean code and proved 30,300 intermediate theorems while translating Andrew Wiles’
AI.info Team ·
13 million lines of Lean code now stand between one of mathematics’ most famous theorems and a computer’s final approval. Anthropic says Claude produced the first complete, end-to-end, computer-checked formalization of Fermat’s Last Theorem in 11 days, turning Andrew Wiles’s celebrated human proof into a machine-readable artifact that Lean can inspect one logical step at a time.
Claude did not discover a new proof of the theorem. Wiles, working with Richard Taylor, established Fermat’s Last Theorem in the 1990s after more than three centuries of failed attempts. Anthropic’s achievement is different: its researchers used a network of Claude agents to translate the existing argument into Lean, fill in thousands of omitted details, and produce a version that a proof assistant could check without relying on a human referee’s judgment.
The result is enormous. Claude proved 30,300 intermediate theorems during the project, with 29,500 appearing in the final proof. The completed code is more than five times the size of Mathlib, the main community library of formalized mathematics on which the work builds.
Eleven Days to Rebuild a 129-Page Proof
Fermat’s Last Theorem states that no positive integers a, b and c satisfy an + bn = cn when n is greater than 2. Pierre de Fermat wrote the claim in the margin of a copy of Diophantus’s Arithmetica around 1637, adding that he had found a “truly marvelous proof” that the margin could not contain.
Fermat’s alleged proof never surfaced. Wiles presented a proof in a series of lectures in June 1993, but mathematicians found a gap during the verification process. He spent another year repairing the argument with Taylor before publishing the corrected result in May 1995. The published proof ran to 129 pages and depended on advanced ideas from algebraic geometry, number theory and the theory of elliptic curves.
Human mathematicians can read such a proof, fill in routine steps and compare its claims with established results. A proof assistant cannot do that. Lean requires every definition, inference and dependency to appear in a formal language that its kernel can check. A sentence that a mathematician regards as obvious may require a separate theorem, a carefully typed object or several layers of supporting code.
Anthropic says the wider mathematics community expected a full formalization of Fermat’s Last Theorem to take years. Kevin Buzzard, a mathematician at Imperial College London who has led a major community effort to formalize the theorem, reviewed the repository after Claude completed the work.
“This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered.”
Kevin Buzzard, mathematician, Imperial College London
Buzzard’s assessment is about formal verification, not the discovery of new mathematics. Claude follows a simplified version of the proof developed by Henri Darmon, Fred Diamond and Richard Taylor, while also drawing on earlier human-written Lean projects from the Imperial College formalization effort and the separate flt-regular project.
Claude Needed a Shared Map of the Proof
Early attempts failed for a practical reason: the agents lost track of what had already been defined, which statements depended on one another and which parts of the theorem still needed proof. Anthropic says those failed runs contributed about 7 percent of the non-boilerplate lines in the final artifact, but the larger lesson came from the coordination problem.
The successful run used Prove2Me, an open collaborative platform developed by Tianyi Peng and collaborators at Columbia University. The system maintained a directed acyclic graph of theorem statements, allowing agents to identify unfinished dependencies and select new targets without repeatedly reconstructing the project’s state.
Prove2Me also separated theorem statements from their proofs. That arrangement let the agents compile smaller units, work in parallel and reuse established results without forcing every task to carry the full project in memory. Natural-language descriptions attached to theorem statements gave the agents another way to search for relevant results and choose a shorter route through the argument.
Dozens of Claude agents worked on separate portions of the formalization. Some defined mathematical objects, others proved intermediate lemmas, and others used those lemmas to attack progressively harder statements. Anthropic says the campaign consumed roughly six billion output tokens from an internal research model comparable to its Claude Fable 5.1 system.
Human involvement remained limited but important. Peng supplied occasional high-level directions, including instructions such as “Jacobian as a scheme sounds high priority” and “push [the] Mazur [theorem] to be done soon.” Those prompts did not replace the individual proof steps. They helped determine which branch of the dependency graph deserved attention next.
Lean Checked the Statement, Not the Story Around It
The public repository defines Fermat’s Last Theorem for natural numbers and includes a final build target that checks the theorem’s dependencies. The target fails if the proof relies on an added axiom, an unfinished placeholder such as sorry, or several forms of unchecked computation. Anthropic says the finished theorem rests on Lean’s three standard axioms: propositional extensionality, quotient soundness and classical choice.
Researchers also ran the code through Lean’s comparator tool. Comparator checked that the theorem proved by the repository matched Mathlib’s own statement of Fermat’s Last Theorem and replayed the proof through the Lean kernel. A second checker, nanoda, independently accepted an export of the same environment after processing more than 1 million declarations without errors.
The repository records the scale of the verification effort. Building the complete project required all 60,475 modules to compile. The comparator replay took about 14 hours and 46 minutes in Anthropic’s reported run, while the full build took 5 hours and 32 minutes using 96 parallel jobs. The project required substantial hardware: Anthropic reports peak memory usage of 153 gigabytes for the build and 230 gigabytes for comparator.
Those checks establish that the formal statement follows from the permitted foundations, provided users trust the Lean kernel, the independent checker and the surrounding software and hardware. They do not establish that every theorem name accurately describes the mathematics a human reader might expect. Anthropic’s repository states that the generated names and labels are machine-oriented and that the formal statement, rather than its name, determines what has been proved.
That distinction matters. Formal verification can show that a chain of typed definitions and deductions is internally valid. It cannot tell a reader whether an intermediate theorem captures the intended mathematical idea, whether the exposition is intelligible or whether a short, elegant argument has been buried beneath layers of generated code.
The Achievement Is Verification, Not Mathematical Discovery
Anthropic draws a direct contrast with recent AI work on the Riemann hypothesis, where researchers presented systems that generated novel mathematical material. Fermat’s Last Theorem was already proved by Wiles. Claude’s contribution was to formalize the existing proof at a level of detail that a computer could check.
Formalization has long served as a second route to confidence in difficult mathematics. Thomas Hales’s proof of the Kepler conjecture spent years in review before a large team created the Flyspeck project to verify it. Grigori Perelman’s work on the Poincaré conjecture required several lengthy expositions before mathematicians accepted its details. Human review remains essential for understanding those results, but it is slow and vulnerable to missed gaps.
Claude’s Fermat project places that tension in a sharper form. A computer can process millions of declarations without tiring, yet the resulting artifact is far too large for a mathematician to read as a conventional proof. The system makes formal checking faster in one sense while creating a new demand for tools that explain what the machine checked.
Anthropic says the project could make it practical to produce a formalized companion for future mathematical papers, especially papers containing long arguments or extensive computational components. A formal proof would not replace a human-readable exposition. It would provide a separate object that researchers could compile, inspect and replay when assessing the claims.
Researchers will still have to decide how much of that process can be automated without weakening mathematical understanding. The Fermat repository itself warns that formalized code is written to be checked rather than read. That limitation is not a defect in Lean; it reflects the difference between a proof designed for human comprehension and one designed for a deterministic verifier.
A New Test for AI-Generated Mathematics
Anthropic’s experiment also changes the unit of measurement for AI mathematics. The headline figure is not a theorem that Claude discovered, but a large body of code that survived several forms of mechanical checking. The relevant question becomes whether an AI system can sustain a long formal project, preserve dependencies across thousands of tasks and recover from failed attempts.
On that test, the system’s architecture mattered as much as the model. Prove2Me supplied the shared state, the theorem graph supplied the work plan and Lean supplied the final arbiter. Without those pieces, Anthropic says, early agents repeatedly lost the thread of the project.
Claude’s completed formalization is now available in the public Anthropic GitHub repository, alongside the Lean sources, the verification scripts and a browser-readable version of the proof. The repository contains pages for roughly 29,511 theorems and 1,450 definition modules, giving researchers a way to trace the formal dependency chain rather than treating the 13 million lines as an opaque block.
Fermat’s theorem therefore enters the machine age in an unusual form: the mathematics is nearly 400 years old, Wiles’s proof is more than 30 years old, and the new artifact is a vast computer-checked reconstruction. Its most concrete result is not a new answer to Fermat’s question. It is a public Lean project that a computer can build, replay and reject if any formal step fails.