Document Open Access Logo

Fermat’s Last Theorem for Regular Primes (Short Paper)

Authors Alex J. Best , Christopher Birkbeck , Riccardo Brasca , Eric Rodriguez Boidi

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.36.pdf
  • Filesize: 0.63 MB
  • 8 pages

Document Identifiers

Author Details

Alex J. Best
  • King’s College London, UK
Christopher Birkbeck
  • University of East Anglia, Norwich, UK
Riccardo Brasca
  • Université Paris Cité, France
Eric Rodriguez Boidi
  • King’s College London, UK

Funding

  • Best, Alex J.: AB. was supported by NWO Vidi grant 639.032.613.

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 As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. Johan Commelin, Adam Topaz, et al. The Liquid Tensor Experiment. Github, 2022. URL: https://github.com/leanprover-community/lean-liquid.
  6. 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.
  7. 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.
  8. Ashvni Narayanan. Formalization of p-adic L-functions in Lean 3, 2023. URL: https://arxiv.org/abs/2302.14491.
  9. Talia Ringer. Proof Repair. PhD thesis, U. Washington, 2021. URL: https://www.proquest.com/dissertations-theses/proof-repair/docview/2568297410/se-2.
  10. 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.
  11. Lawrence C. Washington. Introduction to cyclotomic fields, volume 83 of Graduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1997. Google Scholar
  12. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact