Formal Proof of the Group Law for Edwards Elliptic Curves
Algebraic Geometry
2020-04-28 v1
Abstract
This article gives an elementary computational proof of the group law for Edwards elliptic curves. The associative law is expressed as a polynomial identity over the integers that is directly checked by polynomial division. Unlike other proofs, no preliminaries such as intersection numbers, Bezout's theorem, projective geometry, divisors, or Riemann Roch are required. The proof of the group law has been formalized in the Isabelle/HOL proof assistant.
Cite
@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}
}
Comments
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