Fermat's Last Theorem in Lean 4

Fermat's Last Theorem, proved in Lean 4

A reader's guide to the tree: what is proved, by which route, and how the 29,511 theorems hang together. Every name links to a page with the exact Lean statement, what it cites, what cites it, and its place under the theorem.

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

The default build target FinalCheck.lean makes the build fail unless the proof rests on exactly Lean's three standard axioms:

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

open the theorem's page → the route, step by step landmark graph README

FLT n0 Fermat's Last Theorem n1 Fermat's Last Theorem (Mathlib's formulation) s0 n1->s0 n2 Fermat's Last Theorem for prime exponents p ≥ 5 s1 n2->s1 n3 Frey package from a counterexample of exponent p ≥ 5 s2 n3->s2 n4 No Frey package exists n4->s2 n5 Irreducibility of the mod-p torsion module of the Frey curve s3 n5->s3 n6 Modularity of the Frey curve n6->s3 n7 Level lowering to Γ₀(2) for the Frey curve n7->s3 n8 Vanishing of weight-2 cusp forms of level 2 n8->s3 s0->n0 s1->n1 s2->n2 s3->n4
The top of the proof. Each small square is one proof step: the theorem below it is proved from exactly the premises above it (these are the import Theorems.Thm_… lines of its proof module). FreyPackage.no_frey_package combines irreducibility, modularity, level lowering and the vanishing of S₂(Γ₀(2)) into a contradiction. Click any card.

The route

The argument is that of Frey, Serre, Ribet, Wiles and Taylor–Wiles, largely as in Darmon–Diamond–Taylor, run as a proof by contradiction. The chapters below reproduce the project's route document (the repository's own documents are under Documents), one page per step, each followed by the exact statements of the theorems it names. Named classical theorems are proved in the strength the argument needs; §7 says exactly what that is.

1From the elementary statement to a prime exponent p ≥ 5

3 named theorems

2The Frey package and the four-way contradiction

5 named theorems

3Irreducibility of the mod-p representation of the Frey curve

11 named theorems

4Modularity of semistable elliptic curves

17 named theorems

5Level lowering

10 named theorems

6No cusp forms of weight 2 and level 2

1 named theorem

7Exact strength: how the named theorems differ from the textbook

1 named theorem

The numbers

29,511theorems, each with a statement file and a proof file
1,450definition modules
106,853citation edges between theorems
46deepest shortest path from the theorem
117longest citation chain
8,230theorems proved from Mathlib and definitions alone
49landmark theorems named in the route documents

Largest namespaces by number of theorems: ModularCurve 7,711, AlgebraicGeometry 3,322, CerednikDrinfeld 2,376, AutomorphicForm 2,336, AlgebraicCurve 1,577, LanglandsTunnell 1,543, WeierstrassCurve 1,003, NumberField 766, CuspForm 692, GoodReductionJacobian 674, groupCohomology 361, ValuationSubring 337, HopfAlgebra 333, Algebra 302.

How to use these pages