Formal Proof of the Group Law for Edwards Elliptic Curves

Thomas Hales, Rodrigo Raya

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…