Anthropic publishes full machine-checked proof of Fermat's Last Theorem in Lean 4

Anthropic has released a repository containing a complete, machine-checked proof of Fermat's Last Theorem in Lean 4. The proof builds on Mathlib version 4.33.0 and Lean 4.33.1, which includes kernel soundness fixes from 2026. Its structure follows the classical Frey–Serre–Ribet–Wiles–Taylor-Wiles chain, and a PROOF-PATH.md file maps every step to the corresponding Lean theorem.

The from-scratch lake build comprises 60,475 modules, with every statement verified by the Lean kernel. Axiomatic dependencies are limited to Lean's three standard axioms — propext, Classical.choice, and Quot.sound — with no sorry statements, no additional axioms, and no native_decide. The file FinalCheck.lean enforces this constraint via #guard_msgs and #print axioms; the build fails if any further dependency appears.

Two independent tools confirmed correctness. leanprover/comparator 4.33.0 compared the built environment against a Challenge.lean file that states the theorem using only Mathlib. It verified that the proven statement and all constants it references match the challenge exactly, that no extra axioms are present, and that the entire proof — including Mathlib — re-checks in the kernel. A second independent kernel, nanoda 0.4.13 written in Rust, consumed an export of the same environment via lean4export and checked 1,052,234 statements without errors. Four minor patches were applied to nanoda — one for progress output and three to accelerate definitional equality search — none of which alter any typing rule.

The public HTML export, approximately 390 megabytes, renders the entire repository as static web pages: one page per each of the 29,511 theorems showing the exact statement, citations, and dependencies; a browsable dependency graph; one page per each of the 1,450 definition modules; a search box over theorem and definition names; a landmark theorem graph; and rendered versions of README.md, PROOF-PATH.md, and ATTRIBUTION.md with cross-links. The folder is included in the repository itself, so a clone or ZIP download already contains it.

The maintainers classify the project as a research artifact that is not maintained and does not accept contributions. No module contains axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def, or #eval, except for Challenge.lean, which uses sorry intentionally and is not part of the checked package. The tools verify that the theorem follows from the three standard axioms assuming trust in the kernel and the checkers; what no tool can verify is whether every intermediate theorem actually means what its name suggests — that judgment is left to the reader, and PROOF-PATH.md notes the exact strength at which each classical result is proved.