Merge branch 'main' of github.com:ImperialCollegeLondon/FLT

.github/workflows/push.yml

@@ -68,8 +68,9 @@ jobs:
       - name: Build blueprint
         uses: xu-cheng/texlive-action@v2
         with:
-          scheme: full
+          docker_image: ghcr.io/xu-cheng/texlive-full:20231201
           run: |
+            export PIP_BREAK_SYSTEM_PACKAGES=1
             apk update
             apk add --update make py3-pip git pkgconfig graphviz graphviz-dev gcc musl-dev
             git config --global --add safe.directory $GITHUB_WORKSPACE
@@ -106,4 +107,4 @@ jobs:
 
       - name: Make sure the cache works
         run: |
-          mv docs/docs .lake/build/doc
+          mv docs/docs .lake/build/doc

FLT/Basic/Reductions.lean

@@ -1,7 +1,7 @@
 import Mathlib.Data.PNat.Basic
 import Mathlib.NumberTheory.FLT.Four
-import Mathlib.Tactic.NormNum.Prime
-import Mathlib.AlgebraicGeometry.EllipticCurve.Point
+import Mathlib.Tactic
+import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
 import Mathlib.RepresentationTheory.Basic
 import Mathlib.RingTheory.SimpleModule
 

GENERAL.md

@@ -2,7 +2,7 @@
 
 ## What is Fermat's Last Theorem?
 
-Fermat's Last Theorem (see [https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem](https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem) for more details) is the claim that if x,y,z,n are positive integers and n is at least 3, then x^n + y^n can never equal z^n. The question is so simple that Diophantus, who lived nearly 2000 years ago, could have understood it. It was raised by Pierre de Fermat in 1637, and finally resolved over 350 years later by Andrew Wiles, assisted by Richard Taylor. One extraordinary thing about the proof is that even though the statement of the theorem involves only the counting numbers (some of the simplest mathematical objects), all known proofs involve much deeper mathematics, including but by no means limited to the theory of elliptic curves, modular forms, finite flat group schemes, and Galois representations. Moreover, even though the theorem statement is of a highly arithmetic nature, all known proofs use many other branches of mathematics, borrowing from algebra, cohomology, geometry, and both real and p-adic analysis. A proof, if written out in full from the axioms of mathematics, would occupy several thousand pages.
+Fermat's Last Theorem (see [https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem](https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem) for more details) is the claim that if x,y,z,n are positive integers and n is at least 3, then x^n + y^n can never equal z^n. The question is so simple that Diophantus, who lived nearly 2000 years ago, could have understood it. It was raised by Pierre de Fermat in 1637, and finally resolved over 350 years later by Andrew Wiles, assisted by Richard Taylor. One extraordinary thing about the proof is that even though the statement of the theorem involves only the counting numbers (some of the simplest mathematical objects), all known proofs involve much deeper mathematics, including but by no means limited to the theory of elliptic curves, modular forms, finite flat group schemes, and Galois representations. Moreover, even though the theorem statement is of a highly arithmetic nature, all known proofs use many other branches of mathematics, borrowing from algebra, geometry, and both real and p-adic analysis. Any of the known proofs, if written out in full from the axioms of mathematics, would occupy several thousand pages.
 
 ## What is Lean?
 

blueprint/requirements.txt

@@ -1,5 +1,8 @@
 # https://github.com/pyinvoke/invoke/issues/891
 invoke==2.2.0
 plasTeX @ git+https://github.com/plastex/plastex.git
-leanblueprint @ git+https://github.com/utensil/leanblueprint.git@lean4-only-dev
+plastexdepgraph @ git+https://github.com/PatrickMassot/plastexdepgraph.git
+plastexshowmore @ git+https://github.com/PatrickMassot/plastexshowmore.git
+leanblueprint @ git+https://github.com/PatrickMassot/leanblueprint.git
 watchfiles==0.16.1
+pandoc==2.3

blueprint/src/chapter/frey.tex

@@ -8,7 +8,7 @@ \section{Hardly ramified representations}
 
 We make the following definition (this is not in the literature but it is a useful concept for us). We discuss the meaning of some of the concepts involved afterwards.
 
-\begin{definition} Let $p\geq5$ be a prime. A representation $\rho: \GQ\to \GL_2(\Z/p\Z)$ is said to be \emph{hardly ramified} if it satisfies the following four axioms:
+\begin{definition}\label{hardly_ramified} Let $p\geq5$ be a prime. A representation $\rho: \GQ\to \GL_2(\Z/p\Z)$ is said to be \emph{hardly ramified} if it satisfies the following four axioms:
   \begin{enumerate}
   \item $\det(\rho)$ is the mod $p$ cyclotomic character;
   \item $\rho$ is unramified outside $2p$;
@@ -19,5 +19,5 @@ \section{Hardly ramified representations}
 
 The theorem we want to discuss in this section is:
 
-\begin{theorem} If $\rho$ is the Galois representation on the $p$-torsion of the Frey curve coming from a Frey package, then $\rho$ is hardly ramified.
+\begin{theorem}\label{frey_curve_hardly_ramified}\uses{hardly_ramified} If $\rho$ is the Galois representation on the $p$-torsion of the Frey curve coming from a Frey package, then $\rho$ is hardly ramified.
 \end{theorem}

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "e403f680f0beb8610c29e6f799132e8be880554e",
+   "rev": "0d0ac1c43e1ec1965e0806af9e7a32999ea31096",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
+   "rev": "24a4e8fea81999723bfc38bebf7adc86c2f26c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
+   "inputRev": "v0.0.25",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -46,10 +46,19 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "7d051a52c49ac25ee5a04c7a2a70148cc95ddab3",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "555fddebd3b21542478319c662bc1be696f9178c",
+   "rev": "b4d01dc2afec51cc2bac52b1c1636666672bbe4c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lakefile.lean

@@ -20,9 +20,8 @@ def weakLeanArgs : Array String :=
     #["-DwarningAsError=true"]
   else
     #[]
-    
+
 package FLT where
-  moreServerArgs := moreServerArgs
 
 require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
 
@@ -33,5 +32,8 @@ require «doc-gen4» from git
 
 @[default_target]
 lean_lib FLT where
-  moreLeanArgs := moreLeanArgs
-  weakLeanArgs := weakLeanArgs
+  globs := #[
+    .andSubmodules `FLT
+    ]
+--  moreLeanArgs := moreLeanArgs
+--  weakLeanArgs := weakLeanArgs

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0-rc2
+leanprover/lean4:v4.5.0-rc1