1. Reduction to a prime p ≥ 5

1. Reduction to a prime p ≥ 5. fermat_last_theorem follows in one line from FLT.fermatLastTheorem : FermatLastTheorem (Mathlib's formulation), whose proof applies Mathlib's FermatLastTheorem.of_odd_primes (using exponent 4) and fermatLastTheoremThree and hands a prime p ≥ 5 to FreyPackage.fermatLastTheoremFor_of_five_le, proved from exactly FreyPackage.of_counterexample and FreyPackage.no_frey_package.

Quoted from the route of the proof in PROOF-PATH.md of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

The theorem itself, which the repository's web pages place before this step, then the landmarks they place in it, in the order this step names them:

Theoremfermat_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

Quoted from Theorems/Thm_fermat_last_theorem.lean, line 128 of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0: the file's text from the end of its imports and attribute lines to the top-level :=.

Aliases on the repository's web pages: “Fermat's Last Theorem”, “FLT”.

PROOF-PATH.md names it in 1. Reduction to a prime p ≥ 5.

Lean

fermat_last_theorem, stated in Theorems/Thm_fermat_last_theorem.lean, line 128 and proved in P2M/Sol/S_fermat_last_theorem.lean. Read at commit 6e837e75, without running Lean.

Sources

Leanfermat_last_theorem

Uses 1

Proof usesFreyPackage.fermatLastTheoremFor_of_five_le

TheoremFreyPackage.fermatLastTheoremFor_of_five_le #

open WeierstrassCurve WeierstrassCurve.Affine WeierstrassCurve.Affine.Point
open CuspForm ModularFormClass UpperHalfPlane
theorem FreyPackage.fermatLastTheoremFor_of_five_le (p : ℕ) (pp : p.Prime) (hp5 : 5 ≤ p) : FermatLastTheoremFor p