论文标题
Mordell椭圆形曲线上的形式化类小组计算和积分点
Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
论文作者
论文摘要
二磷酸方程是数量理论中流行而活跃的研究领域。在本文中，我们考虑Mordell方程，该方程的形式为$ y^2 = x^3+d $，其中$ d $是A（给定的）非零整数编号，并且必须确定整数中的所有解决方案，并且必须确定$ x $的所有解决方案。解决此问题的一种非元素方法是通过下降和班级组解决。沿着这些线条，我们在lean 3中正式化了mordell方程的分辨率，以$ d <0 $的几个实例。为了实现这一目标，我们需要从数字理论中形式化其他几种理论，这些理论也很有趣，例如理想的规范，二次字段和戒指，以及对班级编号的明确计算。此外，我们引入了新的计算策略，以便在二次戒指及其他地区进行有效的计算。
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.
