License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.36
URN: urn:nbn:de:0030-drops-184115
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18411/
Best, Alex J. ;
Birkbeck, Christopher ;
Brasca, Riccardo ;
Rodriguez Boidi, Eric
Fermat’s Last Theorem for Regular Primes (Short Paper)
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.
BibTeX - Entry
@InProceedings{best_et_al:LIPIcs.ITP.2023.36,
author = {Best, Alex J. and Birkbeck, Christopher and Brasca, Riccardo and Rodriguez Boidi, Eric},
title = {{Fermat’s Last Theorem for Regular Primes}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {36:1--36:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18411},
URN = {urn:nbn:de:0030-drops-184115},
doi = {10.4230/LIPIcs.ITP.2023.36},
annote = {Keywords: Fermat’s Last Theorem, Cyclotomic fields, Interactive theorem proving, Lean}
}
