Anthropic releases machine-checked Lean 4 proof of Fermat's Last Theorem

A complete machine-checked proof

Anthropic has published a GitHub repository presenting a complete, machine-checked proof of Fermat's Last Theorem in Lean 4, and it surfaced on Hacker News's front page. According to the repository's README, the argument is the classical chain of Frey, Serre, Ribet, Wiles and Taylor–Wiles, built on Mathlib with pinned toolchain versions (Lean 4.33.1, which the README notes includes the 2026 kernel soundness fixes). The work is released under the Apache License 2.0 and framed as a research artifact that is not maintained and accepts no contributions.

The formalized statement, declared in Theorems/Thm_fermat_last_theorem.lean, says that for every natural number n with 3 ≤ n and all positive naturals a, b and c, a^n + b^n ≠ c^n. The README points out that the statement uses Lean's built-in naturals and arithmetic — its only Mathlib ingredient is exponentiation on ℕ, which Mathlib defines as Lean's own — and the default build target also derives Mathlib's FermatLastTheorem statement from the result.

Three layers of checking

The README describes a verification chain designed to be independently repeatable. A from-scratch lake build compiled all 60,475 modules, with every declaration checked by the Lean kernel. The default target uses #guard_msgs to fail the build unless the proof depends on exactly Lean's three standard axioms — propext, Classical.choice and Quot.sound — and a scan found no sorry, added axioms, native_decide or other escape hatches in any packaged module.

A second tool, leanprover's comparator, checked the proved statement against a challenge file written using only Mathlib, confirming that the statement and every constant it mentions match the challenge and that the whole proof, Mathlib included, replays through the kernel. Its verdict, quoted in the README: "Your solution is okay!"

Third, nanoda, an independent Lean kernel written in Rust, accepted an export of the full environment, checking 1,052,234 declarations with no errors. The authors applied four small patches to nanoda for progress output and faster definitional-equality search, and state that none adds, removes or weakens a typing rule.

The README is candid about what is not checked: the result holds given trust in the kernel (or nanoda) and the checking tools, and no tool can confirm that each intermediate theorem means what its name suggests. PROOF-PATH.md maps each classical step to the Lean theorem carrying it. Reproduction is not casual — the reference build took 5 hours 32 minutes at 96 parallel jobs with a 153 GB memory peak, and the comparator run close to 15 hours.

AI agents on community foundations

The Lean sources, per the README, were produced by AI agents building on human-written open-source Lean, "with Lean as the arbiter", and are written to be checked rather than read: names are machine-generated and carry pipeline labels rather than mathematical meaning. The project incorporates material from the Imperial College London FLT project led by Kevin Buzzard — the Frey package, Galois representations, deformation theory and patching — plus the flt-regular proof of Kummer's theorem and Mathlib, with ATTRIBUTION.md listing the 106 files containing borrowed material. An html/ folder of roughly 390 MB renders everything as offline web pages, including a page for each of the 29,511 theorems with expandable dependency graphs.

A conflicting account

The two sources disagree. A dev.to post published minutes before the repository surfaced argues that formalizing FLT in Lean remains an ongoing community effort under Buzzard, that a 2025 paper by Best and colleagues covered only the special case of regular primes, and that Claude's documented Lean work concerned a result related to the Riemann zeta function — hence no completed FLT formalization should be credited to Claude. The repository, published under Anthropic's account and openly building on the Imperial College project, appeared after that assessment and does not name a specific model. It invites exactly the resolution a skeptic would ask for: re-run the builds and checkers and see what the machines accept.

Why it matters

If the checks survive independent reproduction, one of mathematics' most famous theorems joins the small group with a fully machine-checked proof, and the trust base shrinks to the Lean kernel, three standard axioms and a short list of tools, cross-checked by a second kernel. That matters beyond pure mathematics: it shows correctness at scale being established by verification rather than readability or reputation, whether the code was written by people or AI agents. For proof assistants, a project of this size stress-tests kernels, comparators and export tooling in practice. And for AI-assisted mathematics it sets a useful precedent — the deliverable is not plausible-looking prose but a proof the machine accepts, with the residual assumptions stated plainly.