Claude Formalizes Fermat’s Last Theorem: 11 Days of Autonomous Work, Lean Verification, and AI for Advanced Mathematics

Anthropic says Claude produced the first complete computer-checked proof of Fermat’s Last Theorem, translating the modern proof into Lean so that a proof assistant can verify every logical dependency rather than relying on human mathematical review alone.

The project took 11 days of largely autonomous work, generated about 13 million lines of Lean, and proved roughly 30,300 theorems along the way, with about 29,500 intermediate theorems used in the final proof. Anthropic reports that dozens of Claude agents collaborated through a multi-agent workflow rather than one model producing the entire formalization in a single sequence.

The achievement should be interpreted precisely. Claude did not discover Fermat’s Last Theorem or replace Andrew Wiles’s 1995 mathematical breakthrough. The novelty is the end-to-end formalization and machine verification of a proof whose complexity had made full formalization a multi-year research objective.

The work also provides a detailed case study in how agentic AI can handle extremely large technical projects when the orchestration layer gives many agents a shared dependency graph, searchable intermediate results, fast compilation, and a mechanism for recovering from failed proof attempts.

··········

CLAUDE COMPLETED AN END-TO-END LEAN FORMALIZATION THAT HAD BEEN EXPECTED TO TAKE YEARS.

The important result is a machine-checkable mathematical artifact, not a new statement of Fermat’s theorem.

Fermat’s Last Theorem states that no positive integers a, b, and c satisfy aⁿ + bⁿ = cⁿ for any integer n greater than two. Wiles proved the theorem in the 1990s using deep results from modern number theory, but a conventional human proof is not automatically readable by a proof assistant.

Formalization requires every hidden dependency, omitted algebraic step, imported theorem, type relationship, and logical implication to be expressed in a language that the kernel can check. Human mathematical prose routinely skips steps that experts consider obvious; Lean does not. This is why formalizing a major modern proof can become a software-engineering project at a scale comparable to a large codebase.

Anthropic reports that Claude’s final artifact is more than five times the size of Mathlib, the main Lean mathematics library on which the project depends. The system proved 30,300 theorems during the campaign and used about 29,500 of them in the final dependency structure.

........

Metric	Anthropic-reported result	Technical significance
Project duration	11 days	A task expected to require years of coordinated formalization was completed in under two weeks.
Lean code	~13 million lines	The artifact is larger than many production software systems and more than 5× Mathlib by line count.
Theorems proved	~30,300 total; ~29,500 used	The final proof depends on a very large machine-verifiable graph of intermediate results.
Agent structure	Dozens of collaborating Claude agents	Parallelization allowed separate agents to define concepts, prove sub-results, and reuse completed work.
Model	Internal research model roughly comparable to Claude Fable 5.1	The result was produced with a general-purpose research model rather than a narrow theorem prover alone.
Token use	~6 billion output tokens	The project demonstrates capability at very large inference scale and also shows that autonomous formalization remains computationally intensive.

........

··········

PROVE2ME TURNED A FAILED MULTI-AGENT APPROACH INTO A COORDINATED PROOF CAMPAIGN.

The orchestration system was as important as raw model capability because the agents initially lost track of project state.

Anthropic describes several early attempts that stalled because agents accumulated too much local context, lost awareness of which results had already been proved, duplicated work, and stopped collaborating effectively. Those failed attempts still contributed roughly seven percent of the non-boilerplate code in the final proof, but the overall workflow was not reliable until the project moved onto Prove2Me.

Prove2Me is an open collaborative platform developed by Tianyi Peng and collaborators at Columbia University. Its central abstraction is a directed acyclic graph of theorem statements. Instead of asking an agent to remember the entire proof, the platform exposes unresolved dependencies and lets agents choose tractable nodes in the graph, prove them, and make those results available to other agents.

The platform also separates theorem statements from proof implementations so Lean compilation can be distributed more efficiently, and it maintains natural-language descriptions of theorem statements to improve search and reuse. These design choices reduce context-window pressure and make parallel work practical.

Human mathematical direction was limited but not zero. Anthropic says Tianyi Peng occasionally supplied high-level prioritization, such as identifying important objects or pushing particular theorems to completion. The agents performed the detailed formalization work inside that scaffold.

This separation between human project direction and machine execution is significant for professional agent systems. Long-running AI work becomes more reliable when the environment externalizes state, dependencies, intermediate outputs, ownership, and validation instead of expecting the language model to maintain the entire project mentally inside its context window.

··········

THE FINAL PROOF WAS CHECKED AT MULTIPLE LEVELS, INCLUDING LEAN’S KERNEL AND AN INDEPENDENT SECOND KERNEL.

Formal verification changes the trust model because the final mathematical claim is checked by small deterministic systems rather than accepted from the language model.

Anthropic’s public repository documents several verification layers. A from-scratch build used Lean 4.33.1 and compiled Mathlib from source; the Lean kernel checked every declaration. The repository reports 60,475 modules in the build.

The proof was also checked with the Lean comparator against a challenge statement written using Mathlib. That comparison confirmed that the proved theorem matched Mathlib’s statement of Fermat’s Last Theorem and that the proof did not silently replace the target with an easier proposition.

A second independent Lean kernel, nanoda, accepted an exported version of the same environment and checked more than one million declarations without errors. Anthropic also states that the proof uses only Lean’s three standard axioms.

This layered approach is crucial when AI writes the formal proof. The language model can hallucinate while drafting Lean just as it can hallucinate prose, but code that does not type-check or a theorem that does not follow from the permitted axioms cannot pass the proof kernel. The trusted computing base therefore becomes far smaller than the generative system that created the artifact.

........

Verification layer	What was checked	What it protects against
Lean build	All declarations compiled under Lean 4.33.1 with Mathlib built from source	Rejects invalid proof terms, broken dependencies, and type errors.
Lean kernel	Every declaration in the formal environment	Ensures the proof follows the kernel’s logical rules rather than model-generated prose.
Comparator	The final theorem statement against Mathlib’s FLT statement	Prevents success through proving a subtly different or weakened theorem.
Axiom check	Only Lean’s standard axioms are used	Makes hidden untrusted assumptions visible at the logical level.
nanoda	Independent kernel replay of the exported environment	Reduces dependence on a single proof-checking implementation.
Human expert review	Kevin Buzzard reviewed the artifact and its mathematical significance	Adds domain-level scrutiny around architecture, provenance, and usefulness beyond kernel correctness.

........

··········

FORMALIZATION COULD BECOME THE VERIFICATION LAYER FOR AI-GENERATED MATHEMATICS.

The larger implication is that AI can generate mathematical work faster only if verification scales with generation.

The mathematical value of this project is therefore different from a model solving an unsolved conjecture. Its strongest contribution is evidence that large bodies of existing mathematics can potentially be translated into machine-checkable form much faster than traditional manual formalization allowed.

That capability matters because AI systems are already increasing the volume of proposed proofs, conjectures, computational experiments, and research drafts. Human peer review does not scale linearly with that output. A formal proof assistant can verify logical correctness automatically once the mathematics has been expressed in a formal language.

The workflow may also change how mathematical research is authored. A researcher could develop a human-readable proof for explanation while an AI system simultaneously maintains a Lean version for verification. Errors in definitions, dependencies, and intermediate lemmas could then be discovered earlier, before publication or peer review.

There are still important limits. Formal verification establishes that a theorem follows from stated axioms and formalized dependencies; it does not guarantee that a theorem is scientifically interesting, that the chosen definitions capture the intended real-world concept, or that a 13-million-line proof is understandable to humans. Anthropic itself argues that formal proofs should complement rather than replace human-readable mathematical exposition.

The compute profile is also substantial. Roughly six billion output tokens for one project means the economics of fully autonomous formalization still depend on model efficiency, orchestration quality, compilation infrastructure, and the value of the mathematical target. Anthropic notes, however, that smaller formalization projects have already been completed with ordinary Claude Max subscriptions when multiple agents collaborate through the same scaffold.

The Fermat project is therefore best understood as a systems result: a general-purpose model, a multi-agent harness, a shared proof graph, a deterministic theorem prover, and independent verification combined into one pipeline. The model generated the work, but the surrounding architecture made the work tractable and trustworthy.

Primary sources: Anthropic’s research announcement and the public proof repository.

·····

FOLLOW US FOR MORE.

·····

·····

DATA STUDIOS

·····

[datastudios.org]