Edwards 椭圆曲线群律的形式化证明
代数几何
2020-04-28 v1
摘要
本文给出 Edwards 椭圆曲线群律的一个初等计算证明。结合律被表述为整系数上的多项式恒等式，并通过多项式除法直接验证。与其他证明不同，无需诸如交集数、Bezout 定理、射影几何、除子或 Riemann Roch 等预备知识。该群律证明已在 Isabelle/HOL 证明辅助器中形式化。
引用
@article{arxiv.2004.12030,
title = {Formal Proof of the Group Law for Edwards Elliptic Curves},
author = {Thomas Hales and Rodrigo Raya},
journal= {arXiv preprint arXiv:2004.12030},
year = {2020}
}
备注
This article overlaps with arXiv:1610.05278. We make this a separate arXiv submission because a second author has been added, the results from the earlier article have been formalized in this article, and material has been cut to meet conference page limits