The proof of Fermat's Last Theorem

This file contains the "main spine" of the proof of Fermat's Last Theorem.

The strategy of the proof is to prove the theorem via a series of reductions. In other words, we will define mathematical statements B_1=FLT, B_2, B_3, B_4, ..., up to around B_{12}, and then prove that B_2 implies B_1, B_3 implies B_2, B_4 implies B_3 etc etc, and then ultimately that B_{12} is true.

def FLT.Bosses.B1 : Prop

B1 is the statement of FLT.

Equations

• FLT.Bosses.B1 = FermatLastTheorem

def FLT.Bosses.B2 : Prop

B2 is the statement that FLT is true for primes p ≥ 5.

Equations

• FLT.Bosses.B2 = ∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p

def FLT.Bosses.B3 : Prop

B3 is the statement that there is no Frey Package. A Frey package is 4 integers a,b,c,p satisfying a^p+b^p=c^p and some other conditions (for example p is prime and at least 5, a,b,c are pairwise coprime etc). These conditions guarantee that the associated Frey curve Y^2=X(X-a^p)(X+b^p) is semistable.

Equations

• FLT.Bosses.B3 = IsEmpty FreyPackage

def FLT.Bosses.B4 : Prop

B4 is the statement that if E is the Frey curve attached to a Frey package (a,b,c,p), then E[p] is a reducible Galois representation.

Equations

• FLT.Bosses.B4 = ∀ (P : FreyPackage), let E := P.freyCurve; let p := P.p; have this := ⋯; have ρbar := E.galoisRep p ⋯; ¬ρbar.IsIrreducible

theorem FLT.Bosses.B2_implies_B1 : B2 → B1

theorem FLT.Bosses.B3_implies_B2 : B3 → B2

theorem FLT.Bosses.B4_implies_B3 : B4 → B3

theorem FLT.Bosses.B4_proof : B4

theorem FLT.Bosses.B3_proof : B3

theorem FLT.Bosses.B2_proof : B2

theorem FLT.Bosses.B1_proof : B1

theorem flt : FermatLastTheorem