@InProceedings{10.1007/978-3-030-51054-1_15,
	author="Hales, Thomas
	and Raya, Rodrigo",
	editor="Peltier, Nicolas
	and Sofronie-Stokkermans, Viorica",
	title="Formal Proof of the Group Law for Edwards Elliptic Curves",
	booktitle="Automated Reasoning",
	year="2020",
	publisher="Springer International Publishing",
	address="Cham",
	pages="254--269",
	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, B{\'e}zout'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.",
	isbn="978-3-030-51054-1"
}
