Garmelon/whiteprint
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Set up FLT example

Browse source
This commit is contained in:
Joscha 2025-08-02 16:30:46 +02:00
parent d462aad554
commit 3cf236c5df
6 changed files with 325 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

94
example/01_introduction.typ Normal file
View file

@ -0,0 +1,94 @@
#import "common.typ": *
= Introduction
Fermat's Last Theorem is the statement that if $a, b, c, n$ are positive whole
numbers with $n >= 3$, then $a^n + b^n != c^n$. It is thus a statement about a
family of Diophantine equations ($a^3 + b^3 = c^3, a^4 + b^4 = c^4, ...$).
Diophantus was a Greek mathematician who lived around 1800 years ago, and he
would have been able to understand the statement of the theorem (he knew about
positive integers, addition and multiplication).
Fermat's Last Theorem was explicitly raised by Fermat in 1637, and was proved by
Wiles (with the proof completed in joint work with Taylor) in 1994. There are
now several proofs but all of them go broadly in the same direction, using
elliptic curves and modular forms.
Explaining a proof of Fermat's Last Theorem to Lean is in some sense like
explaining the proof to Diophantus; for example, the proof starts by observing
that before we go any further it's convenient to first invent/discover zero and
negative numbers, and one can point explicitly at places in Lean's source code
#link(
"https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Prelude.lean#L1049",
)[here] and #link(
"https://github.com/leanprover/lean4/blob/260eaebf4e804c9ac1319532970544a4e157c336/src/Init/Data/Int/Basic.lean#L45",
)[here] where these things happen. However we will adopt a more efficient
approach: we will assume all of the theorems both in Lean and in its mathematics
library #link("https://github.com/leanprover-community/mathlib4")[mathlib], and
proceed from there. To give some idea of what this entails: mathlib at the time
of writing contains most of an undergraduate mathematics degree and parts of
several relevant Masters level courses (for example, the definitions and basic
properties of #link(
"https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.html",
)[elliptic curves] and #link(
"https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/ModularForms/Basic.html",
)[modular forms] are in mathlib). Thus our task can be likened to teaching a
graduate level course on Fermat's Last Theorem to a computer.
== Which proof is being formalised?
At the time of writing, these notes do not contain anywhere near a proof of FLT,
or even a sketch proof. Over the next few years, we will be building parts of
the argument, following a strategy constructed by Taylor, taking into account
Buzzard's comments on what would be easy or hard to do in Lean. The proof uses
refinements of the original Taylor--Wiles method by Diamond/Fujiwara,
Khare--Wintenberger, Skinner--Wiles, Kisin, Taylor and others --- one could call
it a 21st century proof of the theorem. We shall furthermore be assuming many
nontrivial theorems without proof, at least initially. For example we shall be
assuming the existence of Galois representations attached to weight 2 Hilbert
modular forms, Langlands' cyclic base change theorem for $"GL"_2$, Mazur's
theorem bounding the torsion subgroup of an elliptic curve over the rationals,
and several other nontrivial results which were known by the end of the 1980s.
The first main goal of the project is to state, and then prove, a modularity
lifting theorem; the proof of such a theorem was the key breakthrough introduced
in Wiles' 1994 paper which historically completed the proof of FLT. We will not
be proving the original Wiles--Taylor--Wiles modularity lifting theorem, but
instead will prove a more general result which works for Hilbert modular forms.
We shall say more about the exact path we're taking in #todo[Chapter 4].
== The structure of this blueprint
The following chapter of the blueprint, @first-reduction, explains how to reduce
FLT to two highly nontrivial statements about the $p$-torsion in a certain
elliptic curve (the Frey curve). It mostly comprises of some basic reductions
and the introduction of the Frey curve.
The chapter after that, #[chapter 3], goes into more details about elliptic
curves, however we need so much material here that somehow the top-down approach
felt quite overwhelming at this point. For example even the basic claim that the
$p$-torsion in the Frey curve curve is a 2-dimensional mod $p$ Galois
representation feels like quite a battle to formalise, and proving that it is
semistable and unramified outside $2p$ is even harder. Several people are
working on the basic theory of elliptic curves, and hopefully we will be able to
make more progress on this "top-down" approach later.
The next chapter, #todo[chapter 4], is an _extremely_ sketchy overview of how
the rest of the proof goes. There is so much to do here that I felt that there
was little point continuing with this; definition after definition is missing.
All of the remaining chapters are experiments, and most of them are what I am
currently calling "mini-projects". A mini-project is a bottom-up project,
typically at early graduate student level, with a concrete goal. The ultimate
goal of many of these projects is to actually get some result into mathlib. We
have had one success so far --- the Frobenius mini-project is currently being
PRed to mathlib by Thomas Browning. Currently most of my efforts are going into
running mini-projects, with the two most active ones currently being the adeles
mini-project and the quaternion algebra mini-project. These projects do not
logically depend on each other for the most part, and one can pick and choose
how one reads them.
We finish with an appendix, which is again very sketchy, and comprises mostly of
a big list of nontrivial theorems many of which we will be assuming without
proof in the FLT project, or at least not prioritising until we have proved the
modularity lifting theorem assuming them.

220
example/02_first_reduction.typ Normal file
View file

@ -0,0 +1,220 @@
#import "common.typ": *
= First reductions of the problem <first-reduction>
== 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". 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 neither reducible or irreducible, a
contradiction.
== Reduction to $n >= 5$ and prime
#lemma(
lean: <FermatLastTheorem.of_odd_primes>,
)[
If there is a counterexample to Fermat's Last Theorem, then there is a
counterexample $a^p + b^p = c^p$ with an odd prime $p$.
][
Note: this proof is #link(
"https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/FLT/Four.html#FermatLastTheorem.of_odd_primes",
)[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 = k p$ 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 <= n$ by assumption, so $n = 4 k$
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 #link(
"https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/FLT/Four.html#fermatLastTheoremFour",
)[`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$;
#lemma(
lean: <fermatLastTheoremThree>,
)[
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 #link(
"https://pitmonticone.github.io/FLT3/blueprint/dep_graph_document.html",
)[here]).
]
#corollary(
lean: <FLT.of_p_ge_5>,
uses: (<fermatLastTheoremThree>, <FermatLastTheorem.of_odd_primes>),
)[
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 >= 5$.
][
Follows from the previous two lemmas.
]
== Frey packages
For convenience we make the following definition.
#definition(
lean: <FLT.FreyPackage>,
)[
A _Frey package_ $(a, b, c, p)$ is three pairwise-coprime nonzero integers
$a$, $b$, $c$, with $a eq.triple 3 thick (mod 4)$ and
$b eq.triple 0 thick (mod 2)$, and a prime $p >= 5$, such that
$a^p + b^p = c^p$.
]
Our next reduction is as follows:
#lemma(
lean: <FLT.FreyPackage.of_not_FermatLastTheorem_p_ge_5>,
uses: (<FLT.FreyPackage>,),
)[
If Fermat's Last Theorem is false for $p >= 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.
]
== Galois representations and elliptic curves
To continue, we need some of the theory of elliptic curves over $QQ$. 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 $QQ$ if we want to keep track of the field where the
coefficients of $f(X)$ lie). More generally if $k$ is any field then there is a
concept of an elliptic curve over $k$, again defined by a (slightly more
general) plane cubic curve $F(X, Y) = 0$.
If $E$ is an elliptic curve over a field $k$, and if $K$ is any field which is a
$k$-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". 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. We
shall use $+$ to denote the group law. This 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.
#lemma(
lean: <WeierstrassCurve.Points.map>,
)[
If $E$ is an elliptic curve over a field $k$, and if $K$ and $L$ are two
fields which are $k$-algebras, and if $f : K -> L$ is a $k$-algebra
homomorphism, the map from $E(K)$ to $E(L)$ induced by $f$ is an additive
group homomorphism.
][
The equations defining the group law are ratios of polynomials with
coefficients in $k$, and such things behave well under $k$-algebra
homomorphisms.
]
This construction is functorial (it sends the identity to the identity, and
compositions to compositions).
#lemma(
lean: <WeierstrassCurve.Points.map_id>,
uses: (<WeierstrassCurve.Points.map>,),
)[
The group homomorphism $E(K) -> E(K)$ induced by the identity map $K -> K$ is
the identity group homomorphism.
][
An easy calculation.
]
#lemma(
lean: <WeierstrassCurve.Points.map_comp>,
uses: (<WeierstrassCurve.Points.map>,),
)[
If $K -> L -> M$ are $k$-algebra homomorphisms then the group homomorphism
$E(K) -> E(M)$
induced by the map $K -> M$ is the composite of the map $E(K) -> E(L)$ induced
by $K -> L$ and the map $E(L) -> E(M)$ induced by the map $L -> M$.
][
Another easy calculation.
]
Thus if $f : K -> L$ is an isomorphism of fields, the induced map $E(K) -> E(L)$
is an isomorphism of groups, with the inverse isomorphism being the map
$E(L) -> E(K)$ induced by $f^-1$. This construction thus gives us an action of
the multiplicative group $"Aut"_k(K)$ of $k$-automorphisms of the field $K$ on
the additive abelian group $E(K)$.
#definition(
lean: <WeierstrassCurve.galoisRepresentation>,
uses: (<WeierstrassCurve.Points.map_id>, <WeierstrassCurve.Points.map_comp>),
)[
If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a
$k$-algebra, then the group of $k$-automorphisms of $K$ acts on the additive
abelian group $E(K)$.
]
In particular, if $overline(QQ)$ denotes an algebraic closure of the rationals
(for example, the algebraic numbers in $CC$) and if
$"Gal"(overline(QQ) slash QQ)$ denotes the group of field isomorphisms
$overline(QQ) -> overline(QQ)$, then for any elliptic curve $E$ over $QQ$ we
have an action of $"Gal"(overline(QQ) slash QQ)$ on the additive abelian group
$E(overline(QQ))$.
We need a variant of this construction where we only consider the $n$-torsion of
the curve, for $n$ a positive integer. Recall that if $A$ is any additive
abelian group, and if $n$ is a positive integer, then we can consider the
subgroup $A[n]$ of elements $a$ such that $n a = 0$. If a group $G$ acts on $A$
via additive group isomorphisms, then there will be an induced action of $G$ on
$A[n]$.
#definition(
lean: <WeierstrassCurve.torsionGaloisRepresentation>,
uses: (<WeierstrassCurve.galoisRepresentation>,),
)[
If $E$ is an elliptic curve over a field $k$ and $K$ is a field and a
$k$-algebra, and if $n$ is a natural number, then the group of
$k$-automorphisms of $K$ acts on the additive abelian group $E(K)[n]$ of
$n$-torsion points on the curve.
]
If furthermore $n = p$ is prime, then $A[p]$ is naturally a vector space over
the field $ZZ slash p ZZ$, and thus it inherits the structure of a mod $p$
representation of $G$. Applying this to the above situation, we deduce that if
$E$ is an elliptic curve over $QQ$ then $"Gal"(overline(QQ) slash QQ)$ acts on
$E(overline(QQ))[p]$ and this is the _mod $p$ Galois representation_ attached to
the curve $E$.
In the next section we apply this theory to an elliptic curve coming from a
counterexample to Fermat's Last theorem.

2
example/common.typ Normal file
View file

@ -0,0 +1,2 @@
#import "whiteprint.typ": *
#let todo(body) = text(fill: red, body)

7
example/main.typ Normal file
View file

@ -0,0 +1,7 @@
#import "whiteprint.typ": *
#show: init-whiteprint
#show "mathlib": `mathlib`
#include "01_introduction.typ"
#include "02_first_reduction.typ"

1
example/whiteprint.py Symbolic link
View file

@ -0,0 +1 @@
../whiteprint.py

1
example/whiteprint.typ Symbolic link
View file

@ -0,0 +1 @@
../whiteprint.typ