Statement of Fermat's Last Theorem

This file states Fermat's Last Theorem. We provide a statement over a general semiring with specific exponent, along with the usual statement over the naturals.

Main definitions

• FermatLastTheoremWith R n: The statement that only solutions to the Fermat equation a^n + b^n = c^n in the semiring R have a = 0, b = 0 or c = 0.

Note that this statement can certainly be false for certain values of R and n. For example FermatLastTheoremWith ℝ 3 is false as 1^3 + 1^3 = (2^{1/3})^3, and FermatLastTheoremWith ℕ 2 is false, as 3^2 + 4^2 = 5^2.

• FermatLastTheoremFor n : The statement that the only solutions to a^n + b^n = c^n in ℕ have a = 0, b = 0 or c = 0. Again, this statement is not always true, for example FermatLastTheoremFor 1 is false because 2^1 + 2^1 = 4^1.

• FermatLastTheorem : The statement of Fermat's Last Theorem, namely that the only solutions to a^n + b^n = c^n in ℕ when n ≥ 3 have a = 0, b = 0 or c = 0.

History

Fermat's Last Theorem was an open problem in number theory for hundreds of years, until it was finally solved by Andrew Wiles, assisted by Richard Taylor, in 1994 (see [A. Wiles, Modular elliptic curves and Fermat's last theorem][Wiles-FLT] and [R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras][Taylor-Wiles-FLT]). An ongoing Lean formalisation of the proof, using mathlib as a dependency, is taking place at https://github.com/ImperialCollegeLondon/FLT .

def FermatLastTheoremWith (α : Type u_1) [Semiring α] (n : ℕ) : Prop

Statement of Fermat's Last Theorem over a given semiring with a specific exponent.

Equations

• FermatLastTheoremWith α n = ∀ (a b c : α), a ≠ 0 → b ≠ 0 → c ≠ 0 → a ^ n + b ^ n ≠ c ^ n

def FermatLastTheoremFor (n : ℕ) : Prop

Statement of Fermat's Last Theorem over the naturals for a given exponent.

Equations

• FermatLastTheoremFor n = FermatLastTheoremWith ℕ n

def FermatLastTheorem : Prop

Statement of Fermat's Last Theorem: a ^ n + b ^ n = c ^ n has no nontrivial natural solution when n ≥ 3.

This is now a theorem of Wiles and Taylor--Wiles; see https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of a proof.

Equations

• FermatLastTheorem = ∀ n ≥ 3, FermatLastTheoremFor n

theorem fermatLastTheoremFor_zero : FermatLastTheoremFor 0

theorem not_fermatLastTheoremFor_one : ¬FermatLastTheoremFor 1

theorem not_fermatLastTheoremFor_two : ¬FermatLastTheoremFor 2

theorem FermatLastTheoremWith.mono {α : Type u_1} [Semiring α] [NoZeroDivisors α] {m : ℕ} {n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremWith α m) : FermatLastTheoremWith α n

theorem FermatLastTheoremFor.mono {m : ℕ} {n : ℕ} (hmn : m ∣ n) (hm : FermatLastTheoremFor m) : FermatLastTheoremFor n

theorem fermatLastTheoremWith_nat_int_rat_tfae (n : ℕ) : [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

theorem fermatLastTheoremFor_iff_nat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℕ n

theorem fermatLastTheoremFor_iff_int {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℤ n

theorem fermatLastTheoremFor_iff_rat {n : ℕ} : FermatLastTheoremFor n ↔ FermatLastTheoremWith ℚ n

theorem fermatLastTheoremWith_of_fermatLastTheoremWith_coprime {n : ℕ} {R : Type u_2} [CommSemiring R] [IsDomain R] [DecidableEq R] [NormalizedGCDMonoid R] (hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n) : FermatLastTheoremWith R n

To prove Fermat Last Theorem in any semiring that is a NormalizedGCDMonoid one can assume that the gcd of {a, b, c} is 1.

theorem dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT {n : ℕ} {p : ℤ} (hp : Prime p) {a : ℤ} {b : ℤ} {c : ℤ} (hpa : p ∣ a) (hpb : p ∣ b) (HF : a ^ n + b ^ n + c ^ n = 0) : p ∣ c

theorem isCoprime_of_gcd_eq_one_of_FLT {n : ℕ} {a : ℤ} {b : ℤ} {c : ℤ} (Hgcd : {a, b, c}.gcd id = 1) (HF : a ^ n + b ^ n + c ^ n = 0) : IsCoprime a b