← All papers
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
cs.LO
Sep 30, 2022 · v2
TL;DR
Formalizes class group computations in Lean 3 to solve Mordell elliptic curve equations.
Abstract
Determining all integer solutions to a Mordell equation y^2 = x^3 + d for a nonzero integer d is a classical problem. We describe a non-elementary approach involving resolution via descent and class groups, and formalize in Lean 3 the resolution of Mordell equations for several instances of d < 0. To accomplish this, we formalize ideal norms, quadratic fields and rings, and explicit computations of the class number. We also introduce new computational tactics to carry out efficiently computations in quadratic rings and beyond.
Problem
Determining all integer solutions to Mordell equations y^2 = x^3 + d is a classical problem that requires non-elementary algebraic number theory (class groups, descent), and these methods have not been formally verified.
Approach
The authors formalize in Lean 3 a resolution of Mordell equations via descent and class groups. They formalize ideal norms, quadratic fields and rings, and explicit class number computations. New computational tactics are introduced to carry out computations in quadratic rings efficiently.
Results
Several instances of Mordell equations for d < 0 are resolved formally in Lean 3, with machine-verified class group computations confirming the solutions.