Document Open Access Logo

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

Authors David Kurniadi Angdinata , Junyan Xu

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.6.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Author Details

David Kurniadi Angdinata
  • London School of Geometry and Number Theory, UK
Junyan Xu
  • Cancer Data Science Laboratory, National Cancer Institute, Bethesda, MD, USA

Funding

This work was supported by the Engineering and Physical Sciences Research Council [EP/S021590/1], EPSRC Centre for Doctoral Training in Geometry and Number Theory (London School of Geometry and Number Theory), University College London. This research was supported in part by the Intramural Research Program of the Center for Cancer Research, National Cancer Institute, NIH.

Acknowledgements

We thank the Lean community for their continual support. We thank the mathlib contributors, especially Anne Baanen, for developing libraries this work depends on. We thank Marc Masdeu and Michael Stoll for proposing alternative proofs. DKA would like to thank Kevin Buzzard for his guidance and Mel Levin for suggesting the formalisation in the first place.

Cite AsGet BibTex

David Kurniadi Angdinata and Junyan Xu. An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.6

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
  • Security and privacy → Logic and verification
  • Mathematics of computing → Mathematical software
Keywords
  • formal math
  • algebraic geometry
  • elliptic curve
  • group law
  • Lean
  • mathlib

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. David Angdinata. class_group. URL: https://leanprover-community.github.io/archive/stream/116395-maths/topic/Why.20is.20class_group.2Emk.20so.20slow.3F.html.
  2. A. O. L. Atkin and François Morain. Elliptic curves and primality proving. Mathematics of Computation, 61(203):29-68, 1993. URL: https://doi.org/10.2307/2152935.
  3. Anne Baanen, Sander Dahmen, Ashvni Narayanan, and Filippo Nuccio Mortarino Majno di Capriglio. A formalization of Dedekind domains and class groups of global fields. Journal of Automated Reasoning, 66:611-637, 2022. URL: https://doi.org/10.1007/s10817-022-09644-0.
  4. Evmorfia-Iro Bartzia and Pierre-Yves Strub. A formal library for elliptic curves in the Coq proof assistant. ITP, pages 77-92, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_6.
  5. Richard Borcherds. Hartshorne, Chapter 1.6, Answers to Exercises. URL: https://math.berkeley.edu/~reb/courses/256A/1.6.pdf.
  6. Kevin Buzzard. Thoughts on elliptic curves. URL: https://leanprover-community.github.io/archive/stream/116395-maths/topic/thoughts.20on.20elliptic.20curves.html.
  7. J. W. S. Cassels. Lectures on Elliptic Curves. Cambridge University Press, 1991. Google Scholar
  8. Robin Chapman. Why is an elliptic curve a group? URL: https://mathoverflow.net/q/20623.
  9. Lily Chen, Dustin Moody, Karen Randall, Andrew Regenscheid, and Angela Robinson. Recommendations for discrete logarithm-based cryptography: elliptic curve domain parameters, 2023. URL: https://doi.org/10.6028/NIST.SP.800-186.
  10. The Mathlib Community. mathlib documentation. URL: https://leanprover-community.github.io/mathlib_docs/.
  11. The Mathlib Community. The Lean mathematical library. CPP, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  12. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). CADE, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  13. Pierre Philip du Preez. Understanding EC Diffie-Hellman. URL: https://medium.com/swlh/understanding-ec-diffie-hellman-9c07be338d4a.
  14. David Eisenbud. Commutative algebra with a view toward algebraic geometry. Springer New York, 1995. Google Scholar
  15. Anthony Fox, Mike Gordon, and Joe Hurd. Formalized elliptic curve cryptography. High Confidence Software and Systems, 2006. Google Scholar
  16. Stefan Friedl. An elementary proof of the group law for elliptic curves. Groups Complexity Cryptology, 9(2):117-123, 2017. URL: https://doi.org/10.1515/gcc-2017-0010.
  17. Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. Lecture Notes in Computer Science, 3603:98-113, 2005. URL: https://doi.org/10.1007/11541868_7.
  18. Thomas Hales and Rodrigo Raya. Formal proof of the group law for Edwards elliptic curves. Automated Reasoning, 12167:254-269, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_15.
  19. Kevin Hartnett. Math quartet joins forces on unified theory. URL: https://www.quantamagazine.org/math-quartet-joins-forces-on-unified-theory-20151208/.
  20. Robin Hartshorne. Algebraic Geometry. Springer New York, 1977. Google Scholar
  21. Nicholas Katz and Barry Mazur. Arithmetic Moduli of Elliptic Curves. Princeton University Press, 1985. Google Scholar
  22. Hendrik Lenstra. Factoring integers with elliptic curves. Annals of Mathematics, 126(3):649-673, 1987. URL: https://doi.org/10.2307/1971363.
  23. Marc Masdeu. ell_add_assoc. URL: https://github.com/leanprover-community/mathlib/blob/ell_add_assoc/src/algebraic_geometry/EllipticCurveGroupLaw.lean.
  24. Koji Nuida. An elementary linear-algebraic proof without computer-aided arguments for the group law on elliptic curves. International Journal of Mathematics for Industry, 13(1), 2021. URL: https://doi.org/10.1142/S2661335221500015.
  25. David Russinoff. A computationally surveyable proof of the group properties of an elliptic curve. In Proceedings ACL2Workshop, 2017. URL: https://doi.org/10.4204/EPTCS.249.3.
  26. Joseph Silverman. The Arithmetic of Elliptic Curves. Springer New York, 2009. Google Scholar
  27. Andrew Sutherland. Algebraic proof of the associativity of the elliptic curve group law on curves defined by a short Weierstrass equation, as presented in Lecture 2 of 18.783. URL: https://cocalc.com/share/public_paths/a6a1c2b188bd61d94c3dd3bfd5aa73722e8bd38b.
  28. Laurent Théry. Proving the group law for elliptic curves formally. INRIA, 2007. Google Scholar
  29. Andrew Wiles. The Birch and Swinnerton-Dyer conjecture. URL: https://www.claymath.org/sites/default/files/birchswin.pdf.
  30. Andrew Wiles. Modular elliptic curves and Fermat’s last theorem. Annals of Mathematics, 141(3):443-551, 1995. URL: https://doi.org/10.2307/2118559.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact