Glonce

Anthropic publishes machine-checked proof of Fermat's Last Theorem

researchThe Glonce editorsHacker News🔥66Glonce rating66Impact60Novelty65Relevance80Surprise50Players75Credibility92
Anthropic publishes machine-checked proof of Fermat's Last Theorem

Anthropic has published a GitHub repository containing a complete, machine-checked proof of Fermat's Last Theorem, written in the Lean 4 proof assistant on top of the Mathlib library (Lean 4.33.1, Mathlib v4.33.0 pinned by commit). The argument formalized is the classical one built by Frey, Serre, Ribet, Wiles and Taylor-Wiles; this is not a new mathematical result but a formalization of the existing proof. The Lean sources were produced by AI agents building on human-written open-source Lean code, with the Lean kernel as the final arbiter of correctness. The repository is marked a research artifact: not maintained, and not accepting contributions.

A from-scratch build compiles all 60,475 modules of the repository, and every declaration is checked by the Lean kernel. The build is set up to fail unless the final theorem depends on exactly Lean's three standard axioms, propext, Classical.choice and Quot.sound, with no sorry, no added axiom and no native_decide anywhere in the proof. The theorem itself is stated using only Lean's built-in natural numbers, addition, and the order relations, with a single Mathlib ingredient, exponentiation on natural numbers, which Mathlib defines as identical to Lean's built-in exponentiation.

Two further, independent checks back the build. The leanprover/comparator tool (v4.33.0) checked the build against a separate challenge file that states the theorem using only Mathlib, confirmed the proved statement and every constant it mentions match that challenge exactly, confirmed no other axiom is used, and replayed the whole proof, Mathlib included, through the Lean kernel; its verdict was "Your solution is okay!" Separately, nanoda 0.4.13, an independent Lean kernel written in Rust, checked an exported copy of the same environment and reported 1,052,234 declarations checked with no errors. The authors applied four small patches to nanoda themselves, one adding progress output and three speeding up its equality search, and state that none of the four adds, removes or weakens a typing rule.

Reproducing the full verification is resource-intensive. The authors' own build run took 5 hours 32 minutes at 96 parallel jobs with a peak of 153 GB of memory; the comparator check took 14 hours 46 minutes with a peak of about 230 GB of memory (they recommend allowing 300 GB); and the nanoda check, after a roughly hour-long, 90 GB-memory export step, took about 30 minutes on 16 threads. The build alone needs about 67 GB of disk under .lake/, plus around 220 GB of deletable intermediate C files. The repository also ships an offline-browsable html/ folder, about 390 MB, with a dedicated page for each of 29,511 theorems and 1,450 definition modules, a search box, and a dependency graph of the landmark results.

The authors note a limit on what any of this checking proves: the kernel and the two independent checkers confirm that the final statement follows validly from the three axioms, but no tool can confirm that each intermediate, machine-generated theorem name actually means what it suggests. That judgment is left to a human reader, and the repository's PROOF-PATH.md documents which Lean theorem carries each step of the classical argument and how strong each one is as proved here. The repository credits 106 files containing reused Apache-2.0 code from the Imperial College London FLT project led by Kevin Buzzard and from the flt-regular project, plus 23 files that reproduce Mathlib text directly, all listed with upstream authorship in ATTRIBUTION.md. The source does not say when the proof itself was completed, does not name the specific AI system or agents involved beyond "AI agents," and makes no claim to being the first machine-checked or first Lean proof of the theorem.

Key facts

  • Anthropic published a Lean 4 and Mathlib formalization of Fermat's Last Theorem on GitHub, following the classical Frey-Serre-Ribet-Wiles-Taylor-Wiles argument, with the Lean sources produced by AI agents building on human-written open-source Lean.
  • The from-scratch build compiles all 60,475 modules of the repository, and the final proof is required to depend on exactly Lean's three standard axioms, propext, Classical.choice and Quot.sound, with no sorry, no added axiom and no native_decide.
  • The leanprover/comparator tool matched the proved statement to an independently written challenge file and returned the verdict "Your solution is okay!"; separately, the independent Rust-based nanoda 0.4.13 kernel checked 1,052,234 declarations with no errors.
  • Reproducing the checks is resource-heavy: the authors' own build took 5 hours 32 minutes (peak 153 GB RAM), the comparator check took nearly 15 hours (peak about 230 GB RAM), and the nanoda check took about 30 minutes after a roughly hour-long export step.
  • The repository ships an offline html/ folder (about 390 MB) with pages for 29,511 theorems and 1,450 definition modules, and credits 106 reused files from Kevin Buzzard's Imperial College London FLT project and flt-regular, plus 23 files that reproduce Mathlib text.

Why it matters

Fermat's Last Theorem was proved by Andrew Wiles and Richard Taylor in the 1990s through a long, human-refereed mathematical argument. Encoding that argument so a machine kernel can check every logical step, rather than a community of referees, is a large-scale formalization exercise: 60,475 compiled modules and 29,511 documented theorems. That it was built by AI agents working on top of an existing open-source proof library is offered as a demonstration of AI-assisted formal mathematics at a scale beyond a toy example, in a domain where correctness can be checked mechanically rather than taken on trust.

Who it affects

The direct audience is the Lean and Mathlib community and formal-methods researchers, who gain a large worked example and reusable Lean material (credited back to the Imperial College London FLT project and flt-regular). More broadly, it is a data point for anyone tracking how far AI systems can go in producing verifiable mathematics, since the correctness of the output here is checked by a kernel rather than asserted.

How to use it

The code is on GitHub (anthropics/fermats-last-theorem) under the Apache License 2.0, explicitly marked as a research artifact that is not maintained and not accepting contributions. It can be browsed without building anything, by opening the bundled html/index.html folder (about 390 MB) in a Chromium-based browser, which works fully offline. Reproducing the actual verification requires Linux or macOS, Lean 4.33.1 via elan, and substantial hardware: about 67 GB of disk for the build, up to roughly 300 GB of memory recommended for the comparator step, and a combined run time on the order of a day across the build, the comparator check and the nanoda check.

How solid is it

The result rests on three separate checks: the Lean kernel accepting the from-scratch build of all 60,475 modules, the leanprover/comparator tool independently confirming the proved statement matches a separately written challenge statement using only stock Mathlib definitions, and the independent nanoda kernel, written in Rust, checking an exported copy of the same environment and finding 1,052,234 declarations with no errors. The four small patches applied to nanoda add progress output and speed, and the authors state none of them touches a typing rule. The final theorem depends on exactly Lean's three standard axioms, propext, Classical.choice and Quot.sound, with no sorry, no added axiom and no native_decide anywhere in the proof. The authors are explicit that this checks logical validity, not that each intermediate theorem's name matches its content: that judgment is left to a human reader, guided by the PROOF-PATH.md documentation of each proof step.

Risks and caveats

This is a formalization of an existing, already-proved theorem, not a new mathematical result. The Lean names inside the proof are machine-generated (labels such as P2M or hexadecimal suffixes) and are described by the authors as pipeline labels rather than mathematics, so where a name and a statement disagree, the statement is what was proved, a point the authors state directly. The source does not say when the proof itself was completed, does not identify the specific AI system or agents beyond "AI agents," and makes no claim of being the first machine-checked or first Lean proof of the theorem. It also does not mention any academic paper or peer-reviewed publication, describing a GitHub repository only. The repository reuses Apache-2.0 code in 106 files from Kevin Buzzard's Imperial College London FLT project and from flt-regular, and reproduces Mathlib text directly in 23 files, all credited in ATTRIBUTION.md; the source does not say that Buzzard or that project participated in or endorsed this repository.

“the build fails unless the proof rests on exactly Lean's three standard axioms (no sorry, no added axiom, no native_decide)”

— the repository's build documentation