13 million lines of proof: AI formalizes Fermat’s theorem

How the formalization was organized

Anthropic says Claude worked on the formalization for eleven days, producing roughly 13 million lines of Lean and more than 30,000 proved intermediate theorems. The system used Prove2Me, infrastructure that decomposed the main objective into a graph of dependent subproblems that could be solved and reused. Roughly 29,500 proved results were used later in the construction. The scale demonstrates more than code generation: completing the task required managing dependencies, memory, verification and recovery across an unusually long research trajectory.

Lean served as a rigorous judge. Every accepted fragment had to pass the kernel’s checks against explicit rules and the available libraries. The model could propose steps, repair failures and search for alternatives, but a fluent explanation could not persuade the checker to accept an invalid term. Anthropic’s source reports the execution and project statistics. The conclusion that task architecture mattered as much as raw model capability is Mateusz’s editorial interpretation, grounded in the roles of the Prove2Me graph and Lean’s verifier.

What was actually checked

The result is a formal artifact intended to pass Lean’s checks from its assumptions and imported components through to the final theorem. Anthropic reports that the project produced a codebase more than five times the size of the contemporary Mathlib and consumed about six billion output tokens. Much of that material supported search, failed attempts and infrastructure; only a small share of non-boilerplate code from unsuccessful branches entered the final path. Those figures expose the substantial selection cost hidden behind the finished proof.

Machine verification gives strong evidence that the formal record follows the rules of the system, but the guarantee has a precise boundary. The kernel checks whether terms have the required types and whether conclusions follow from declared assumptions. It does not judge historical originality, explanatory quality or whether the formalizer selected the most illuminating route. Trust shifts away from a model’s prose toward a smaller checker, its libraries and the correctness of the correspondence between the formal statement and the mathematical claim people intended to encode.

Why this is not a new proof of Fermat

Claude did not discover a new mathematical idea that solved Fermat’s Last Theorem. The formalization follows established mathematics developed around Andrew Wiles’s proof and depends on existing libraries and work by the Lean community. The novel element is the scale and degree of automation involved in translating that chain into a formal language. Saying that “AI solved Fermat” would therefore be misleading: the theorem had already been proved, while this project produced a computer-checkable representation of a known mathematical route.

Formal success also does not show that 13 million generated lines are easy for people to audit or that every chosen definition is pedagogically ideal. An artifact can be logically correct while remaining extremely difficult to read. Nor does one project demonstrate automatic formalization of any unexplored field of mathematics. The work relied on large computational resources, an existing ecosystem and the structure of this particular problem. General capability will need to be tested on new theorems with different dependencies and less mature supporting libraries.

A two-layer model for publication

Mateusz’s proposed publication model contains two connected layers. The first explains the proof’s idea, major dependencies, intuition and significance for human readers. The second supplies the formal artifact, library versions, reproduction instructions and the result of an independent check. Readers can then understand the argument at an appropriate level while specialists verify the machine record. Anthropic does not present this as a formal publishing standard; it is Mateusz’s editorial proposal for using Lean’s strongest property without abandoning human-readable mathematical communication.

The next meaningful tests should include independent reproduction of the repository, maintenance after library changes and formalizations for which fewer ready-made components exist. Evaluations should measure not only solved goals but also computational cost, manual contribution, reusable library output and reviewability. The deeper breakthrough will arrive when formal certificates become cheaper and broadly accessible while remaining paired with an explanation of why the proof works. Verification can protect correctness, but it should not replace understanding.

A goal shaped by centuries of mathematics and decades of formalization

Fermat’s Last Theorem began with Pierre de Fermat’s note from around 1637, but its modern proof required mathematics unavailable to him. Andrew Wiles presented an argument in 1993; detailed scrutiny found a gap, which he repaired with Richard Taylor before the correct papers appeared in 1995. That history explains why mathematicians distinguish a persuasive narrative from a proof. Even an extraordinary argument may require months of reading, dependency checking and repair of one critical connection. Formal verification addresses that fragility by asking a machine to account explicitly for every link rather than relying on a reader to reconstruct omitted steps.

The ambition to translate Wiles’s route into a computer-checked language predates today’s generative models. Anthropic points to Jan Bergstra’s proposal two decades ago and the community project started at Imperial College London in 2024 under Kevin Buzzard. Claude’s result therefore did not emerge in a vacuum. It entered a mature ecosystem of Lean, Mathlib, blueprints and formal components built by hundreds of people. The new achievement concerns the speed and scale at which established mathematics was integrated, not the erasure of the human proof or the historical work that made its formal expression possible.

What the Lean certificate actually covers

Anthropic’s repository declares the theorem over natural numbers: for an exponent of at least three and positive a, b and c, a to the nth power plus b to the nth power is not equal to c to the nth power. Its default FinalCheck target is designed to fail unless the result depends on exactly the three standard Lean axioms used by the project. The authors also scanned modules for mechanisms that could bypass ordinary checking, including sorry, added axioms, unsafe code and native_decide. This is a description of a precise formal object rather than a claim resting only on a launch announcement.

The Lean kernel checks each declared term against the type system and replays its dependencies down to the foundations. It need not trust the style of an explanation, the author’s reputation or a language model’s confidence. The guarantee is nevertheless conditional: it applies to the statement actually encoded, under specified tool versions and axioms. It cannot automatically decide whether every definition best captures the intended mathematics or whether the route is comprehensible. Formality sharply narrows the space for logical error, but it does not remove the need to understand the exact boundary of the certificate.

Comparator and a second kernel strengthen the trusted base

The authors did more than report that one build passed. Comparator was used to confirm that the final theorem and every constant named in its statement were identical to a challenge expressed only with Mathlib. The environment was then exported and accepted by nanoda, an independent Lean kernel written in Rust; the repository reports more than one million declarations checked without error. Two distinct checking routes reduce the chance that acceptance depends on an accidental property of one implementation. They also expose a smaller and more concrete trusted base for reviewers to inspect.

This evidence still needs a careful label. The artifact’s creators published the checks and their results; public code enables external reproduction, but creator-run logs are not by themselves a complete independent replication. The project applied four small patches to nanoda, described as progress-reporting and performance changes that do not weaken typing rules. A reviewer should inspect those patches, pinned dependencies and scripts rather than reading only the final verdict. Confidence grows through a compact, transparent chain of trust, not through an assumption that any checker or build pipeline is infallible.

The proof’s backbone ends in an impossible modular form

The formalization proceeds by contradiction. A putative counterexample is reduced to a prime exponent of at least five and packaged into normalized data and a Frey curve. Subsequent nodes establish that the associated Galois representation is irreducible and that the curve is modular. This is where purpose-built forms of results associated with Mazur, Langlands–Tunnell and modularity lifting enter the route. The repository’s proof map identifies the exact Lean type carrying each connection, preventing the name of a celebrated theorem from standing in for the particular statement that the formal argument actually uses.

Ribet-style level lowering would then turn the Frey curve into a non-zero weight-two cusp form for Γ₀(2). The final step formally proves that this space is zero, creating the contradiction and excluding the counterexample. `PROOF-PATH.md` also separates the exact strength of each named result from its broader textbook formulation. The project does not claim, for example, to formalize every theorem of Mazur or every version of level lowering; it proves the variants required by this route. That narrowness is an auditing advantage because it makes the true dependency boundary inspectable.

Provenance of inherited code is part of the result

A dedicated `ATTRIBUTION.md` identifies 106 files containing material taken or adapted from the Imperial College London project or `flt-regular`: 54 under definitions and 52 under solutions. Another 23 files reproduce Mathlib text. The inventory records upstream files, authors and an approximate extent of reuse. Those figures do not diminish the agents’ integration work. They reveal the formal capital already available to the campaign and show which components should not be attributed to the new system.

This layer was necessary because agent-assembled Lean files were published without comments, so many upstream headers did not survive at the point of use. The authors reconstructed provenance through code comparison, earlier notes and a licensing table. During the port to Lean 4.33.1, 65 of the 106 inherited files received mechanical lemma-name or proof adjustments, while 41 remained byte-identical. A correctness audit and an authorship audit answer different questions; a credible artifact needs both, especially when a model composes a result from many libraries.

Reproduction is possible but materially expensive

The repository pins Lean 4.33.1 and a specific Mathlib release and documents a build from source. That is a much stronger starting point than an unverifiable screenshot, but the exercise is not lightweight. The instructions call for tens of gigabytes of storage, substantial memory per parallel job and additional resources for Comparator and the nanoda export. Anthropic reports a multi-hour build on a machine running 96 jobs. Those timings and resource figures describe the creator’s infrastructure and should be treated as planning guidance rather than a performance promise for every machine.

The authors also warn that some paths are too long for Windows, so the complete process is intended for Linux or macOS. This operational limitation matters for open verification: an artifact can be public while remaining beyond an ordinary laptop. A mature replication programme should publish file hashes, reproducible environments or precise setup instructions, logs from machines outside the creator’s organization and useful intermediate verdicts. The most persuasive certificate is one that multiple teams can replay without access to the original laboratory’s infrastructure, even if the full check remains too expensive for every individual reader.

A certificate is a versioned snapshot, not an eternal build

The repository pins Lean 4.33.1 and Mathlib 4.33.0 and describes itself as a research artifact that is not maintained or accepting contributions. That choice strengthens reproduction of the published state: a reviewer knows which definitions, kernel fixes and dependencies belong in the check. It does not guarantee that the same source will compile unchanged under a future Lean release. A later toolchain failure would not automatically invalidate the earlier certificate, but it would require a clear distinction between replaying a historical environment and porting the proof into a new ecosystem.

If the formalization is to support later mathematics, it needs a second life beyond the frozen artifact: maintainers, regression tests, explicit records of semantic changes and a route for moving useful components into community libraries. This is an editorial conclusion, not an Anthropic maintenance commitment. A one-time build answers whether a specified term passed specified checkers. Stewardship answers whether other teams can safely import, explain and extend that knowledge as dependencies evolve. Long-term impact will therefore depend not only on the number of generated lines but also on the quality and transparency of that migration.

Readable exposition must evolve beside the formal artefact

A kernel-checked artefact and a text written for people perform different jobs. The former makes it possible to verify mechanically that every step follows from declared definitions, axioms and previously proved results. The latter helps a reader see the strategy: why a particular lemma was chosen, where the main difficulty sits and how a local move contributes to the larger construction. Prose should not become loose promotion for a formal file, and the file should not be treated as a substitute for explanation. A credible publication maintains both tracks together and states precisely which claims the machine-checked boundary covers.

An exposition map provides a practical bridge. It records stable definitions, sketches dependencies among the principal results and links them to exact declaration names in the repository. Each prose section can point to the corresponding artefact location, environment version and assumptions imported from elsewhere. When a formalisation uses a technical device that is convenient for the proof assistant, the commentary should explain its role without presenting it as the only mathematically natural route. Conversely, intuition that is not encoded in the proof must remain labelled as interpretation rather than as something certified by the kernel.

The two materials should share a versioning process. A change to a definition, dependency or proof structure triggers both a link check and an exposition review, because accurate prose can become stale even while the code continues to compile. A reviewer needs a short path from a claim in the article to its formal declaration and back to an explanation of its significance. Good exposition does not simplify by removing accountability. It lowers the cost of entry while preserving the distinction among motivation, mathematical argument and what mechanical verification actually establishes.