2 First reductions of the problem
2.1 Goal
The goal of this chapter is to reduce FLT to a deep theorem of Mazur and a deep theorem of Wiles about a Galois representation.
2.2 Overview
The proof of Fermat’s Last Theorem is by contradiction. We assume that we have a counterexample \(a^n+b^n=c^n\), and manipulate it until it satisfies the axioms of a “Frey package”, a basic concept which we will explain below. From the Frey package we build a Frey curve – an elliptic curve defined over the rationals. We then look at a certain representation of a Galois group coming from this elliptic curve, and finally using two very deep and independent theorems (one due to Mazur, the other due to Wiles) we show that this representation is both reducible and irreducible, the contradiction we seek.
2.3 Reduction to \(n\geq 5\) and prime
If there is a counterexample to Fermat’s Last Theorem, then there is a counterexample \(a^p+b^p=c^p\) with \(p\) an odd prime.
Note: this proof is in mathlib already; we run through it for completeness’ sake.
Say \(a^n + b^n = c^n\) is a counterexample to Fermat’s Last Theorem. Every positive integer is either a power of 2 or has an odd prime factor. If \(n=kp\) has an odd prime factor \(p\) then \((a^k)^p+(b^k)^p=(c^k)^p\) is the counterexample we seek. It remains to deal with the case where \(n\) is a power of 2, so let’s assume this. We have \(3\leq n\) by assumption, so \(n=4k\) must be a multiple of 4, and thus \((a^k)^4=(b^k)^4=(c^k)^4\), giving us a counterexample to Fermat’s Last Theorem for \(n=4\). However an old result of Fermat himself (proved as fermatLastTheoremFour in mathlib) says that \(x^4+y^4=z^4\) has no solutions in positive integers.
Euler proved Fermat’s Last Theorem for \(p=3\);
There are no solutions in positive integers to \(a^3+b^3=c^3\).
The proof in mathlib was formalized by a team from the “Lean For the Curious Mathematician” conference held in Luminy in March 2024 (its dependency graph can be visualised here).
If there is a counterexample to Fermat’s Last Theorem, then there is a counterexample \(a^p+b^p=c^p\) with \(p\) prime and \(p\geq 5\).
Follows from the previous two lemmas.
2.4 Frey packages
For convenience we make the following definition.
A Frey package \((a,b,c,p)\) is three nonzero pairwise-coprime integers \(a\), \(b\), \(c\), with \(a\equiv 3\pmod4\) and \(b\equiv 0\pmod2\), and a prime \(p\geq 5\), such that \(a^p+b^p=c^p\).
Our next reduction is as follows:
If Fermat’s Last Theorem is false for \(p \ge 5\) and prime, then there exists a Frey package.
Suppose we have a counterexample \(a^p+b^p=c^p\) for the given \(p\); we now build a Frey package from this data.
If the greatest common divisor of \(a,b,c\) is \(d\) then \(a^p+b^p=c^p\) implies \((a/d)^p+(b/d)^p=(c/d)^p\). Dividing through, we can thus assume that no prime divides all of \(a,b,c\). Under this assumption we must have that \(a,b,c\) are pairwise coprime, as if some prime divides two of the integers \(a,b,c\) then by \(a^p+b^p=c^p\) and unique factorization it must divide all three of them. In particular we may assume that not all of \(a,b,c\) are even, and now reducing modulo 2 shows that precisely one of them must be even.
Next we show that we can find a counterexample with \(b\) even. If \(a\) is the even one then we can just switch \(a\) and \(b\). If \(c\) is the even one then we can replace \(c\) by \(-b\) and \(b\) by \(-c\) (using that \(p\) is odd).
The last thing to ensure is that \(a\) is 3 mod 4. Because \(b\) is even, we know that \(a\) is odd, so it is either 1 or 3 mod 4. If \(a\) is 3 mod 4 then we are home; if however \(a\) is 1 mod 4 we replace \(a,b,c\) by their negatives and this is the Frey package we seek.
2.5 Galois representations and elliptic curves
To continue, we need some of the theory of elliptic curves over \(\mathbb {Q}\). So let \(f(X)\) denote any monic cubic polynomial with rational coefficients and whose three complex roots are distinct, and let us consider the equation \(E:Y^2=f(X)\), which defines a curve in the \((X,Y)\) plane. This curve (or strictly speaking its projectivisation) is a so-called elliptic curve (or an elliptic curve over \(\mathbb {Q}\) if we want to keep track of the field where the coefficients of \(f(X)\) lie).
If \(E:Y^2=f(X)\) is an elliptic curve over \(\mathbb {Q}\), and if \(K\) is any characteristic zero field (and hence a \(\mathbb {Q}\)-algebra), then we write \(E(K)\) for the set of solutions to \(y^2=f(x)\) with \(x,y\in K\), together with an additional “point at infinity” corresponding morally to \(x=y=\infty \). It is an extraordinary fact, and not at all obvious, that \(E(K)\) naturally has the structure of an additive abelian group, with the point at infinity being the zero element (the identity). Fortunately this fact is already in mathlib. This additive group structure has the property that three distinct points \(P,Q,R\in K^2\) which are in \(E(K)\) will sum to zero if and only if they are collinear.
The group structure behaves well under change of field: if \(E\) is an elliptic curve over \(\mathbb {Q}\) and if \(K\to L\) is a homomorphism of characteristic zero fields then the induced map \(E(K)\to E(L)\) is a group homomorphism. Thus if \(f:K\to L\) is an isomorphism of characteristic zero fields, the induced map \(E(K)\to E(L)\) is an isomorphism of groups, with the inverse isomorphism being the map \(E(L)\to E(K)\) induced by \(f^{-1}\). This construction thus gives us an action of the multiplicative group \(\operatorname{Aut}(K)\) of automorphisms of the field \(K\) on the additive abelian group \(E(K)\), and hence also on the \(n\)-torsion of this group for any positive integer \(n\). In particular, if \(\overline{\mathbb {Q}}\) denotes an algebraic closure of the rationals (for example, the algebraic numbers in \(\mathbb {C}\)) and if \(\operatorname{Gal}(\overline{\mathbb {Q}}/\mathbb {Q})\) denotes the group of field isomorphisms \(\overline{\mathbb {Q}}\to \overline{\mathbb {Q}}\), then for any elliptic curve \(E\) over \(\mathbb {Q}\) we have an action of \(\operatorname{Gal}(\overline{\mathbb {Q}}/\mathbb {Q})\) on the additive abelian group \(E(\overline{\mathbb {Q}})\), and hence on its \(n\)-torsion subgroup \(E(\overline{\mathbb {Q}})[n]\).
If furthermore \(n=p\) is prime, then \(E(\overline{\mathbb {Q}})[p]\) is naturally a vector space over the field \(\mathbb {Z}/p\mathbb {Z}\), and thus it inherits the structure of a mod \(p\) representation of \(\operatorname{Gal}(\overline{\mathbb {Q}}/\mathbb {Q})\). This is the mod \(p\) Galois representation attached to the elliptic curve \(E\). It is well-known to be 2-dimensional. We call this representation \(\rho _{E,p}\).
In the next section we apply this theory to an elliptic curve coming from a counterexample to Fermat’s Last theorem.
2.6 The Frey curve
Recall that a Frey package \((a,b,c,p)\) is simply a prime \(p\geq 5\) and nonzero pairwise-coprime integers \(a,b,c\) satisfying \(a^p+b^p=c^p\) and satisfying the congruences \(a\equiv 3\pmod4\) and \(b\equiv 0\pmod2\). We have shown above that if Fermat’s Last Theorem is false, then a Frey package exists.
Given a Frey package \((a,b,c,p)\), the corresponding Frey curve (considered by Frey and, before him, Hellegouarch) is the elliptic curve over \(\mathbb {Q}\) defined by the equation \(Y^2=X(X-a^p)(X+b^p).\)
Note that the roots of the cubic \(X(X-a^p)(X+b^p)\) are distinct because \(a,b,c\) are nonzero and \(a^p+b^p=c^p\).
Given a Frey package \((a,b,c,p)\) with corresponding Frey curve \(E\), the mod \(p\) Galois representation \(\rho _{E,p}\) associated to this package is the 2-dimensional representation of \(\operatorname{Gal}(\overline{\mathbb {Q}}/\mathbb {Q})\) on \(E(\overline{\mathbb {Q}})[p]\) described above. Frey’s observation is that this mod \(p\) Galois representation has some very surprising properties. We will make this remark more explicit in the next chapter. Here we shall show how these properties can be used to finish the job.
2.7 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?
If \(\rho \) is the mod \(p\) Galois representation associated to a Frey package \((a,b,c,p)\) then \(\rho \) is irreducible.
This follows from a profound and long result of Mazur [ 7 ] 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 [ 9 ] .
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.
If \(\rho \) is the mod \(p\) Galois representation associated to a Frey package \((a,b,c,p)\) then \(\rho \) is reducible.
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.
There is no Frey package.
We deduce
Fermat’s Last Theorem is true. In other words, there are no positive integers \(a,b,c\) and natural \(n\geq 3\) such that \(a^n+b^n=c^n\).
Because we are (for now at least) assuming Mazur’s theorem, we now need to turn our attention to a proof of theorem 2.8. We start on this proof in Chapter 3.