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.

The statement

Theorems/Thm_fermat_last_theorem.lean declares

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

/-- 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

... continue reading