← All papers
Fermat's Last Theorem for Regular Primes
cs.LO
May 15, 2023 · v1
TL;DR
Formalizes the first case of Fermat's Last Theorem for regular primes in Lean with mathlib.
Abstract
We formalise the proof of the first case of Fermat's Last Theorem for regular primes using the Lean theorem prover and its mathematical library 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 mathlib.
Problem
Fermat's Last Theorem for regular primes is an important 19th century result in algebraic number theory that motivated the development of modern algebraic number theory, but it had not been formalized in a proof assistant.
Approach
The authors formalize the proof of the first case of Fermat's Last Theorem for regular primes using Lean and Mathlib. The formalization required dealing with diamonds about characteristic zero fields, problems arising from multiple nested coercions related to number fields, and integration of number-theoretic results with Lean's type system.
Results
The first case of Fermat's Last Theorem for regular primes is fully formalized in Lean with Mathlib, resolving challenges around coercions and characteristic zero field diamonds.