diff --git a/example/01_introduction.typ b/example/01_introduction.typ deleted file mode 100644 index 1258e48..0000000 --- a/example/01_introduction.typ +++ /dev/null @@ -1,94 +0,0 @@ -#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 deleted file mode 100644 index 49bf497..0000000 --- a/example/02_first_reduction.typ +++ /dev/null @@ -1,220 +0,0 @@ -#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 deleted file mode 100644 index ee3361c..0000000 --- a/example/common.typ +++ /dev/null @@ -1,2 +0,0 @@ -#import "whiteprint.typ": * -#let todo(body) = text(fill: red, body) diff --git a/example/main.typ b/example/main.typ deleted file mode 100644 index fffffb0..0000000 --- a/example/main.typ +++ /dev/null @@ -1,7 +0,0 @@ -#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 deleted file mode 120000 index fd5559d..0000000 --- a/example/whiteprint.py +++ /dev/null @@ -1 +0,0 @@ -../whiteprint.py \ No newline at end of file diff --git a/example/whiteprint.typ b/example/whiteprint.typ deleted file mode 120000 index 5a94e8c..0000000 --- a/example/whiteprint.typ +++ /dev/null @@ -1 +0,0 @@ -../whiteprint.typ \ No newline at end of file