LIPIcs.ITP.2023.36.pdf
- Filesize: 0.63 MB
- 8 pages
Document
Fermat’s Last Theorem for Regular Primes (Short Paper)
Authors
Alex J. Best 
,
Christopher Birkbeck ,
Riccardo Brasca ,
Eric Rodriguez Boidi
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
We thank the mathlib community for a lot of useful discussions around our project. We especially thank Ruben Van de Velde for having formalised in Lean a proof of Fermat’s Last Theorem in the case n = 3.
Cite AsGet BibTex
Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi. Fermat’s Last Theorem for Regular Primes (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 36:1-36:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.36
https://doi.org/10.4230/LIPIcs.ITP.2023.36
Abstract
We formalise the proof of the first case of Fermat’s Last Theorem for regular primes using the Lean theorem prover and its mathematical library mathlib. This is an important 19th century result that motivated the development of modern algebraic number theory. Besides explaining the mathematics behind this result, we analyze in this paper the difficulties we faced in the formalisation process and how we solved them. For example, we had to deal with a diamond about characteristic zero fields and problems arising from multiple nested coercions related to number fields. We also explain how we integrated our work to mathlib.
Subject Classification
ACM Subject Classification
- General and reference → Verification
- Computing methodologies → Representation of mathematical objects
- Mathematics of computing → Mathematical software
Keywords
- Fermat’s Last Theorem
- Cyclotomic fields
- Interactive theorem proving
- Lean
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: A case study in functional analysis. In Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, pages 3-20, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-51054-1_1.
- Anne Baanen, Alex J. Best, Nirvana Coppola, and Sander R. Dahmen. Formalized class group computations and integral points on mordell elliptic curves. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 47-62, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575682.
- Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, and Filippo A. E. Nuccio Mortarino Majno di Capriglio. A Formalization of Dedekind Domains and Class Groups of Global Fields. J. Autom. Reason., 66(4):611-637, 2022. URL: https://doi.org/10.1007/s10817-022-09644-0.
- Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising Perfectoid Spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 299-312, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373830.
- Johan Commelin, Adam Topaz, et al. The Liquid Tensor Experiment. Github, 2022. URL: https://github.com/leanprover-community/lean-liquid.
- Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A Metaprogramming Framework for Formal Verification. Proc. ACM Program. Lang., 1(ICFP), August 2017. URL: https://doi.org/10.1145/3110278.
- The mathlib Community. The Lean Mathematical Library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
- Ashvni Narayanan. Formalization of p-adic L-functions in Lean 3, 2023. URL: https://arxiv.org/abs/2302.14491.
- Talia Ringer. Proof Repair. PhD thesis, U. Washington, 2021. URL: https://www.proquest.com/dissertations-theses/proof-repair/docview/2568297410/se-2.
- Richard Taylor and Andrew Wiles. Ring-theoretic properties of certain Hecke algebras. Ann. of Math. (2), 141(3):553-572, 1995. URL: https://doi.org/10.2307/2118560.
-
Lawrence C. Washington. Introduction to cyclotomic fields, volume 83 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1997.
- Andrew Wiles. Modular elliptic curves and Fermat’s last theorem. Ann. of Math. (2), 141(3):443-551, 1995. URL: https://doi.org/10.2307/2118559.