A complete formalization of Fermat's Last Theorem for regular primes in Lean

Best, Alex, Birkbeck, Christopher, Brasca, Riccardo, Rodriguez Boidi, Eric, van de Velde, Ruben and Yang, Andrew (2025) A complete formalization of Fermat's Last Theorem for regular primes in Lean. Annals of Formalized Mathematics, 1. 103–132.

Preview

PDF (hal-04718128) - Published Version Available under License Creative Commons Attribution. Download (1MB) | Preview

Abstract

We formalize a complete proof of the regular case of Fermat's Last Theorem in the Lean4 theorem prover. Our formalization includes a proof of Kummer's lemma, that is the main obstruction to Fermat's Last Theorem for regular primes. Rather than following the modern proof of Kummer's lemma via class field theory, we prove it by using Hilbert's Theorems 90-94 in a way that is more amenable to formalization.

Item Type:	Article
Faculty \ School:	Faculty of Science > School of Engineering, Mathematics and Physics
UEA Research Groups:	Faculty of Science > Research Groups > Algebra, Number Theory, Logic, and Representations (ANTLR)
Related URLs:	https://arxiv.org/abs/2410.01466
Depositing User:	LivePure Connector
Date Deposited:	11 Jul 2025 15:30
Last Modified:	15 Jul 2025 15:34
URI:	https://ueaeprints.uea.ac.uk/id/eprint/99887
DOI:	10.46298/afm.14586

Downloads

Actions (login required)

View Item