Reduction to two big theorems.

Recall that a representation of a group \(G\) on a vector space \(W\) is said to be irreducible if there are precisely two \(G\)-stable subspaces of \(W\), namely \(0\) and \(W\). The representation is said to be reducible otherwise.

Now say \((a,b,c,p)\) is a Frey package. Consider the mod \(p\) representation of \(\operatorname{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\) coming from the \(p\)-torsion in the Frey curve \(Y^2=X(x-a^p)(X+b^p)\) associated to the package. Let's call this representation \(\rho\), and we say that \(\rho\) is the mod \(p\) representation associated to the Frey package \((a,b,c,p)\). Is it irreducible or not?

TheoremMazur#

If \(\rho\) is the mod \(p\) Galois representation associated to a Frey package \((a,b,c,p)\) then \(\rho\) is irreducible.

Proof

This follows from a profound and long result of Mazur (Mazur 1977) from 1977, namely the fact that the torsion subgroup of an elliptic curve over \(\mathbb{Q}\) can have size at most 16. In fact there is still a little more work which needs to be done to deduce the theorem from Mazur's result. A pre-1990 reference for the full proof of this claim is Proposition 6 in §4.1 of (Serre 1987).

Lean

Stated as FreyPackage.mazur; the blueprint marks no proof of it as formalized.

Sources
LeanFreyPackage.mazur
Uses 1 · Used by 1
Statement usesFrey
Used byFreyPackage.false

Note that in the first (pre-2029) phase of the FLT project, we will not be working on a formalization of this result, as it was known in the 1980s. We will however be thinking a lot about the next result, which says the exact opposite.

TheoremWiles,Taylor–Wiles, Ribet,…#

If \(\rho\) is the mod \(p\) Galois representation associated to a Frey package \((a,b,c,p)\) then \(\rho\) is reducible.

Proof

This is the main content of Wiles' magnum opus. We omit the argument for now, although later on in this project we will have a lot to say about a proof of this.

Lean

Stated as FLT.Bosses.B4_proof; the blueprint marks no proof of it as formalized.

Sources
LeanFLT.Bosses.B4_proof
Uses 1 · Used by 1
Statement usesFrey
Used byFreyPackage.false

CorollaryFreyPackage.false#

There is no Frey package.

Proof

Follows immediately from the previous two theorems Mazur and Wiles,Taylor–Wiles, Ribet,….

Lean

Stated as FLT.Bosses.B3_proof; the blueprint marks no proof of it as formalized.

Sources
LeanFLT.Bosses.B3_proof
Uses 2 · Used by 1
Statement usesMazur · Wiles,Taylor–Wiles, Ribet,…
Used byFLT

We deduce

CorollaryFLT#

Fermat's Last Theorem is true. In other words, there are no positive integers \(a,b,c\) and natural \(n\geq3\) such that \(a^n+b^n=c^n\).

Proof

Assume there is a there is a counterexample \(a^n+b^n=c^n\). By Corollary FermatLastTheorem.of_p_ge_5 we may assume that there is also a counterexample \(a^p+b^p=c^p\) with \(p\geq 5\) and prime. Then there is a Frey package \((a,b,c,p)\) by FreyPackage.of_not_FermatLastTheorem_p_ge_5, contradicting Corollary FreyPackage.false.

Lean

Stated as flt; the blueprint marks no proof of it as formalized.

Sources
Leanflt
Uses 3
Proof usesFermatLastTheorem.of_p_ge_5 · FreyPackage.false · FreyPackage.of_not_FermatLastTheorem_p_ge_5

Because we are (for now at least) assuming Mazur's theorem, we now need to turn our attention to a proof of theorem Wiles,Taylor–Wiles, Ribet,…. We start on this proof in Chapter Reducibility of p-torsion of the Frey curve.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.