论文标题
爱德华兹椭圆形曲线的团体法律的正式证明
Formal Proof of the Group Law for Edwards Elliptic Curves
论文作者
论文摘要
本文提供了Edwards椭圆曲线的小组定律的基本计算证明。关联定律表示为多项式划分直接检查整数的多项式身份。与其他证据不同，不需要相交数字，bezout的定理，投射几何形状，除数或riemann roch等初步。伊莎贝尔/HOL证明助理已正式化了集体法的证明。
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.
