anthropics/fermats-last-theorem

# Fermat's Last Theorem in Lean 4

A complete, machine-checked proof of Fermat's Last Theorem in [Lean 4](https://lean-lang.org), built on

[Mathlib](https://github.com/leanprover-community/mathlib4) (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.

## The statement

Theorems/Thm_fermat_last_theorem.lean declares

~~~lean

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

~~~

and the default build target FinalCheck.lean contains

~~~lean

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/

#guard_msgs in

#print axioms fermat_last_theorem

~~~

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.

## How it was verified

Mathlib compiled from source. All 60,475 modules of this repository built, every declaration was checked by the

Lean kernel, and the axioms are as above.

verification/comparator/Challenge.lean, which states the theorem using only Mathlib. It confirmed that the proved

statement and every constant it mentions are identical to the challenge, that no other axiom is used, and that the

whole proof, Mathlib included, replays through the Lean kernel. Verdict: Your solution is okay!

Rust, accepted an export of the same environment (written with lean4export): `Checked 1052234 declarations with no

errors. We built nanoda with four small patches of our own (verification/nanoda/patches/`): one adds progress output and

three speed up its definitional-equality search, without which a few declarations of this proof occupy unmodified

nanoda for many hours each. None of the patches adds, removes or weakens a typing rule.

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.

## Reading the proof in a browser

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).

## Check it yourself

installs Lean 4.33.1 from lean-toolchain), and a network connection: Lake fetches Mathlib from GitHub and compiles

it from source, since no prebuilt Mathlib matches this toolchain (about 13 minutes at 96 jobs).