From 3cf236c5dfeee8b172880d976be259d35937bb42 Mon Sep 17 00:00:00 2001 From: Joscha Date: Sat, 2 Aug 2025 16:30:46 +0200 Subject: [PATCH] Set up FLT example --- example/01_introduction.typ | 94 ++++++++++++++ example/02_first_reduction.typ | 220 +++++++++++++++++++++++++++++++++ example/common.typ | 2 + example/main.typ | 7 ++ example/whiteprint.py | 1 + example/whiteprint.typ | 1 + 6 files changed, 325 insertions(+) create mode 100644 example/01_introduction.typ create mode 100644 example/02_first_reduction.typ create mode 100644 example/common.typ create mode 100644 example/main.typ create mode 120000 example/whiteprint.py create mode 120000 example/whiteprint.typ diff --git a/example/01_introduction.typ b/example/01_introduction.typ new file mode 100644 index 0000000..1258e48 --- /dev/null +++ b/example/01_introduction.typ @@ -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. diff --git a/example/02_first_reduction.typ b/example/02_first_reduction.typ new file mode 100644 index 0000000..49bf497 --- /dev/null +++ b/example/02_first_reduction.typ @@ -0,0 +1,220 @@ +#import "common.typ": * + += First reductions of the problem + +== 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: , +)[ + 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: , +)[ + 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: , + uses: (, ), +)[ + 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: , +)[ + 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: , + uses: (,), +)[ + 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: , +)[ + 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: , + uses: (,), +)[ + The group homomorphism $E(K) -> E(K)$ induced by the identity map $K -> K$ is + the identity group homomorphism. +][ + An easy calculation. +] + +#lemma( + lean: , + uses: (,), +)[ + 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: , + uses: (, ), +)[ + 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: , + uses: (,), +)[ + 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. diff --git a/example/common.typ b/example/common.typ new file mode 100644 index 0000000..ee3361c --- /dev/null +++ b/example/common.typ @@ -0,0 +1,2 @@ +#import "whiteprint.typ": * +#let todo(body) = text(fill: red, body) diff --git a/example/main.typ b/example/main.typ new file mode 100644 index 0000000..fffffb0 --- /dev/null +++ b/example/main.typ @@ -0,0 +1,7 @@ +#import "whiteprint.typ": * + +#show: init-whiteprint +#show "mathlib": `mathlib` + +#include "01_introduction.typ" +#include "02_first_reduction.typ" diff --git a/example/whiteprint.py b/example/whiteprint.py new file mode 120000 index 0000000..fd5559d --- /dev/null +++ b/example/whiteprint.py @@ -0,0 +1 @@ +../whiteprint.py \ No newline at end of file diff --git a/example/whiteprint.typ b/example/whiteprint.typ new file mode 120000 index 0000000..5a94e8c --- /dev/null +++ b/example/whiteprint.typ @@ -0,0 +1 @@ +../whiteprint.typ \ No newline at end of file