HackerPapers

arXiv:2410.01466cs.FL

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

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

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.

arXiv comments
Journal reference
DOI
Subjects
cs.FLFormal Languages and Automata Theory cs.LOLogic in Computer Science math.NTNumber Theory

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Jun 2025 to Jun 2025. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.