// HACKER NEWS — CYBERSECURITY
Fermat's Last Theorem in Lean 4
A complete, machine-checked proof of Fermat's Last Theorem in Lean 4, built on
Mathlib (Lean 4.33.1; Mathlib v4.33.0, pinned by commit in
lakefile.lean). The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles. PROOF-PATH.md names each step
and the Lean theorem that carries it, and the html/ folder presents the whole proof as web pages you can browse
offline (see "Reading the proof in a browser" below).
Research artifact. Not maintained and not accepting contributions.
and the default build target FinalCheck.lean contains
so the build fails unless the proof rests on exactly Lean's three standard axioms (no sorry, no added axiom,
no native_decide). FinalCheck.lean also derives Mathlib's own statement, FermatLastTheorem, from this theorem.
No module contains axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def or #eval
(Challenge.lean uses sorry by design and is not part of the package).
Together, these checks establish that the statement above follows from the three axioms, given trust in the Lean
kernel (or nanoda) and the checking tools. The statement is written with Lean's built-in natural numbers, +, ≤, <
and ≠; its one Mathlib ingredient is ^ on ℕ, which Mathlib defines as Lean's built-in exponentiation, and
comparator checks that every definition the statement mentions is identical to stock Mathlib's. Nothing else in
Mathlib has to be trusted, because the kernel checks everything beneath the statement. What no tool can check is that
each intermediate theorem means what its name suggests; that is for the reader to judge, and PROOF-PATH.md names
the Lean theorem behind each step and states exactly how strong each named classical result is as proved here.
The html/ folder (about 390 MB) presents this repository as static web pages: the route of the proof step by step;
a page for each of the 29,511 theorems (the exact Lean statement, what it cites and what cites it, and an expandable
dependency graph) and for each of the 1,450 definition modules (the full source and which statements use it); a
search box over all theorem and definition names; the landmark theorems as a graph; and README.md, PROOF-PATH.md
and ATTRIBUTION.md rendered with cross-links. The folder is part of this repository, so a clone or a ZIP download
already contains it (if you obtained html/ as a separate archive, unpack it at the repository root). Open
html/index.html in a web browser; everything works offline, with no web server. The pages were machine-tested in a
Chromium-based browser only, and html/README-DOCS.md explains what is quoted from the Lean files and what is
generated (the English summaries and suggested references are generated automatically; the Lean statement is
authoritative).
Lean prints a large number of deprecation and style-linter warnings while building. They do not affect the result.
The build has succeeded when its output ends with
'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] and Build completed successfully. Each
script fetches and builds its checker at a pinned version and exits 0 on success.
FinalCheck.lean is the default target; Theorems/ holds the statements, P2M/Sol/ the proofs (each importing the
statements it cites), Definitions/ the definitions, verification/ the two checks, html/ the web pages described
above and tools/docs-site/ the program that generated them. The Lean sources 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, labels such as P2M or hexadecimal suffixes are pipeline labels rather than mathematics, and where
a name and a statement disagree the statement is what was proved. Comments were removed, apart from upstream notices,
doc strings and citations (listed in ATTRIBUTION.md) and the expected-output comment that #guard_msgs checks.
Copyright 2026 Anthropic, PBC; released under the Apache License 2.0 (LICENSE). Portions