Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

DOI10.1145/3573105.3575682arXiv2209.15492MaRDI QIDQ6412484FDOQ6412484

Authors: Anne Baanen, Alex Best, Nirvana Coppola, Sander R. Dahmen 

Publication date: 30 September 2022

Abstract: Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form $y^2=x^3+d$, where $d$ is a (given) nonzero integer number and all solutions in integers $x$ and $y$ have to be determined. One non-elementary approach for this problem is the resolution via descent and class groups. Along these lines we formalized in Lean 3 the resolution of Mordell equations for several instances of $d<0$. In order to achieve this, we needed to formalize several other theories from number theory that are interesting on their own as well, such as ideal norms, quadratic fields and rings, and explicit computations of the class number. Moreover we introduced new computational tactics in order to carry out efficiently computations in quadratic rings and beyond.

Mathematics Subject Classification ID

Cubic and quartic Diophantine equations (11D25) Quadratic extensions (11R11) Class numbers, class groups, discriminants (11R29) Formalization of mathematics in connection with theorem provers (68V20)

This page was built for publication: Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6412484)