Fermat's Last Theorem for regular primes

Tools

Best, Alex J., Birkbeck, Christopher ORCID: https://orcid.org/0000-0002-7546-9028, Brasca, Riccardo and Boidi, Eric Rodriguez (2023) Fermat's Last Theorem for regular primes.

Full text not available from this repository. (Request a copy)

Abstract

We formalise the proof of the first case of Fermat's Last Theorem for regular primes using the \emph{Lean} theorem prover and its mathematical library \emph{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 \emph{mathlib}.

Item Type:	Article
Additional Information:	Accepted for the 14th International Conference on Interactive Theorem Proving (ITP 2023)
Uncontrolled Keywords:	cs.lo,math.nt,68v20, 03b70,f.4.1
Faculty \ School:	Faculty of Science > School of Mathematics (former - to 2024)
UEA Research Groups:	Faculty of Science > Research Groups > Algebra and Combinatorics (former - to 2024) Faculty of Science > Research Groups > Algebra, Logic & Number Theory
Related URLs:	http://arxiv.org/pdf/2305.08955v1
Depositing User:	LivePure Connector
Date Deposited:	25 May 2023 10:32
Last Modified:	07 Nov 2024 12:48
URI:	https://ueaeprints.uea.ac.uk/id/eprint/92190
DOI:

Actions (login required)

View Item