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

Alex Best; Christopher Birkbeck; Riccardo Brasca; Eric Rodriguez Boidi; Ruben  van de Velde; Andrew Yang

doi:10.46298/afm.14586

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

Alex Best, Christopher Birkbeck, Riccardo Brasca, Eric Rodriguez Boidi, Ruben van de Velde, Andrew Yang

Research output: Contribution to journal › Article › peer-review

12 Downloads (Pure)

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.

Original language	English
Pages (from-to)	103–132
Number of pages	30
Journal	Annals of Formalized Mathematics
Volume	1
DOIs	https://doi.org/10.46298/afm.14586
Publication status	Published - 15 Jul 2025

Access to Document

10.46298/afm.14586Licence: CC BY

hal-04718128Final published version, 1.11 MBLicence: CC BY

https://arxiv.org/abs/2410.01466

Cite this

@article{a93fd385d6d144c9bc6f706532e5fd99,

title = "A complete formalization of Fermat's Last Theorem for regular primes in Lean",

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.",

author = "Alex Best and Christopher Birkbeck and Riccardo Brasca and {Rodriguez Boidi}, Eric and {van de Velde}, Ruben and Andrew Yang",

year = "2025",

month = jul,

day = "15",

doi = "10.46298/afm.14586",

language = "English",

volume = "1",

pages = "103–132",

journal = "Annals of Formalized Mathematics",

publisher = "Episciences",

}

TY - JOUR

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

AU - Best, Alex

AU - Birkbeck, Christopher

AU - Brasca, Riccardo

AU - Rodriguez Boidi, Eric

AU - van de Velde, Ruben

AU - Yang, Andrew

PY - 2025/7/15

Y1 - 2025/7/15

N2 - 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.

AB - 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.

U2 - 10.46298/afm.14586

DO - 10.46298/afm.14586

M3 - Article

VL - 1

SP - 103

EP - 132

JO - Annals of Formalized Mathematics

JF - Annals of Formalized Mathematics

ER -