License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.6
URN: urn:nbn:de:0030-drops-183817
URL: https://drops.dagstuhl.de/opus/volltexte/2023/18381/
Go to the corresponding LIPIcs Volume Portal


Angdinata, David Kurniadi ; Xu, Junyan

An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic

pdf-format:
LIPIcs-ITP-2023-6.pdf (0.8 MB)


Abstract

Elliptic curves are fundamental objects in number theory and algebraic geometry, whose points over a field form an abelian group under a geometric addition law. Any elliptic curve over a field admits a Weierstrass model, but prior formal proofs that the addition law is associative in this model involve either advanced algebraic geometry or tedious computation, especially in characteristic two. We formalise in the Lean theorem prover, the type of nonsingular points of a Weierstrass curve over a field of any characteristic and a purely algebraic proof that it forms an abelian group.

BibTeX - Entry

@InProceedings{angdinata_et_al:LIPIcs.ITP.2023.6,
  author =	{Angdinata, David Kurniadi and Xu, Junyan},
  title =	{{An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18381},
  URN =		{urn:nbn:de:0030-drops-183817},
  doi =		{10.4230/LIPIcs.ITP.2023.6},
  annote =	{Keywords: formal math, algebraic geometry, elliptic curve, group law, Lean, mathlib}
}

Keywords: formal math, algebraic geometry, elliptic curve, group law, Lean, mathlib
Collection: 14th International Conference on Interactive Theorem Proving (ITP 2023)
Issue Date: 2023
Date of publication: 26.07.2023
Supplementary Material: Software (Source Code): https://github.com/alreadydone/mathlib/tree/associativity archived at: https://archive.softwareheritage.org/swh:1:dir:1bd75e80371560806d5f287177a4922b6282f7e2


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI