Fermat's Last Theorem in Lean 4

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

fermat_last_theorem (Theorems/Thm_fermat_last_theorem.lean) is the elementary statement over ℕ quoted in the top-level README. Its proof module is two lines: it applies FLT.fermatLastTheorem : FermatLastTheorem (Theorems/Thm_FLT_fermatLastTheorem.lean), Mathlib's own formulation, which in turn is proved by

theorem solution : FermatLastTheorem := by
  apply FermatLastTheorem.of_odd_primes
  intro p pp p_odd
  by_cases hp5 : 5 ≤ p
  · exact FreyPackage.fermatLastTheoremFor_of_five_le p pp hp5
  · have hp2 := pp.two_le
    interval_cases p
    · exact absurd p_odd (by decide)
    · exact fermatLastTheoremThree
    · exact absurd pp (by decide)

(P2M/Sol/S_FLT_fermatLastTheorem.lean after its preamble; FermatLastTheorem.of_odd_primes, which uses exponent 4 internally, and fermatLastTheoremThree are Mathlib's). Everything else hangs below FreyPackage.fermatLastTheoremFor_of_five_le (p : ℕ) (pp : p.Prime) (hp5 : 5 ≤ p) : FermatLastTheoremFor p, which is proved from exactly two theorems: FreyPackage.of_counterexample and FreyPackage.no_frey_package.

← The route · §2 The Frey package and the four-way contradiction →

How the theorems of this step depend on each other

Green cards are the landmarks named in this section; dashed white cards are landmarks of neighbouring steps they connect to. Premises above conclusions; an arrow may pass through unnamed intermediate theorems. Click a card for its page.

L n0 Fermat's Last Theorem fermat_last_theorem n1 Fermat's Last Theorem for prime exponents p ≥ 5 FreyPackage.fermatLastTheoremFor_of_five_le n1->n0 n2 No Frey package exists FreyPackage.no_frey_package n2->n1 n3 Frey package from a counterexample of exponent p ≥ 5 FreyPackage.of_counterexample n3->n1 n4 Irreducibility of the mod-p torsion module of the Frey curve FreyPackage.Mazur_Frey n4->n2 n5 Modularity of the Frey curve FreyPackage.frey_isModular n5->n2 n6 Level lowering to Γ₀(2) for the Frey curve FreyPackage.level_lowering_to_two n6->n2

Theorems named in this section (3; statement as in the tree, numbers from the import graph)

Fermat's Last Theorem fermat_last_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
29,488 theorems below · cites 1 · cited by 0 · depth 0 · proof 3 lines, 0 helpers
Frey package from a counterexample of exponent FreyPackage.of_counterexample
theorem FreyPackage.of_counterexample (a b c : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (p : ℕ) (pp : p.Prime) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FreyPackage
0 theorems below · cites 0 · cited by 1 · depth 3 · proof 61 lines, 1 helpers
No Frey package exists FreyPackage.no_frey_package
theorem FreyPackage.no_frey_package (P : FreyPackage) : False
29,484 theorems below · cites 4 · cited by 1 · depth 3 · proof 13 lines, 1 helpers

2 theorems of the tree are first reached through this step, in the sense that the first landmark met on a shortest citation path up to fermat_last_theorem is one named in this section. That is a reading aid, not a classification: the infrastructure below modularity and level lowering is largely shared.

← The route · §2 The Frey package and the four-way contradiction →