Towards a Lean proof of Fermat’s Last Theorem

Bibliography

1

Thomas Barnet-Lamb, Toby Gee, David Geraghty, and Richard Taylor. Potential automorphy and change of weight. Ann. of Math. (2), 179(2):501–609, 2014.

2

Armand Borel and W. Casselman, editors. Automorphic forms, representations and \(L\)-functions. Part 1, volume XXXIII of Proceedings of Symposia in Pure Mathematics. American Mathematical Society, Providence, RI, 1979.

3

Armand Borel and W. Casselman, editors. Automorphic forms, representations, and \(L\)-functions. Part 2, volume XXXIII of Proceedings of Symposia in Pure Mathematics. American Mathematical Society, Providence, RI, 1979.

4

J. W. S. Cassels and A. Fröhlich, editors. Algebraic number theory. Academic Press, London; Thompson Book Co., Inc., Washington, DC, 1967.

5

Toby Gee. Modularity lifting theorems. Essent. Number Theory, 1(1):73–126, 2022.

6

Chandrashekhar Khare and Jean-Pierre Wintenberger. Serre’s modularity conjecture. II. Invent. Math., 178(3):505–586, 2009.

7

B. Mazur. Modular curves and the Eisenstein ideal. Inst. Hautes Études Sci. Publ. Math., (47):33–186, 1977. With an appendix by Mazur and M. Rapoport.

8

Laurent Moret-Bailly. Groupes de Picard et problèmes de Skolem. I, II. Ann. Sci. École Norm. Sup. (4), 22(2):161–179, 181–194, 1989.

9

Jean-Pierre Serre. Sur les représentations modulaires de degré \(2\) de \(\operatorname{Gal}(\overline{\mathbb {Q}}/\mathbb {Q})\). Duke Math. J., 54(1):179–230, 1987.

10

Jean-Pierre Serre. Galois cohomology. Springer Monographs in Mathematics. Springer-Verlag, Berlin, english edition, 2002. Translated from the French by Patrick Ion and revised by the author.

11

Joseph H. Silverman. The arithmetic of elliptic curves, volume 106 of Graduate Texts in Mathematics. Springer, Dordrecht, second edition, 2009.

12

Richard Taylor. On the meromorphic continuation of degree two \(L\)-functions. Doc. Math., pages 729–779, 2006.

13

John Voight. Quaternion algebras, volume 288 of Graduate Texts in Mathematics. Springer, 2021. Version v1.0.6u, available at https://jvoight.github.io/quat.html.