• A complete formalization of Fe...

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

Title:
A complete formalization of Fermat's Last Theorem for regular primes in Lean
Authors:
Best, Alex, Birkbeck, Christopher, Brasca, Riccardo, Rodriguez Boidi, Eric, Velde, Ruben van De, Yang, Andrew
Contributors:
Brasca, Riccardo
Source:
Annals of Formalized Mathematics. 1
Publication Status:
Preprint
Publisher Information:
Centre pour la Communication Scientifique Directe (CCSD), 2025.
Publication Year:
2025
Subject Terms:
FOS: Computer and information sciences, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Logic in Computer Science, Formal Languages and Automata Theory (cs.FL), Kummer's lemma, Logic in Computer Science (cs.LO), Number Theory, FOS: Mathematics, Lean, Number Theory (math.NT), Formal Languages and Automata Theory, Mathlib, [MATH.MATH-NT] Mathematics [math]/Number Theory [math.NT], [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Document Type:
Academic journal Article
File Description:
application/pdf
Language:
English
DOI:
10.46298/afm.14586
DOI:
10.48550/arxiv.2410.01466
Access URL:
http://arxiv.org/abs/2410.01466
https://ueaeprints.uea.ac.uk/id/eprint/99887/
Rights:
arXiv Non-Exclusive Distribution
CC BY
Accession Number:
edsair.doi.dedup.....5a79fafc31e1957fb3a27b2a5b55b627
Database:
OpenAIRE

Further Information

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.