2 Search Results for "Stoll, Michael"

Document
DOI: 10.4230/LIPIcs.ITP.2023.6
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic

Authors: David Kurniadi Angdinata and Junyan Xu

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.6},
  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}
}
Document
DOI: 10.4230/DagSemProc.09221.5
Rational Points on Curves of Genus 2: Experiments and Speculations

Authors: Michael Stoll

Published in: Dagstuhl Seminar Proceedings, Volume 9221, Algorithms and Number Theory (2009)

Abstract
I will present results of computations providing statistics on rational points on (small) curves of genus 2 and use them to present several conjectures. Some of them are based on heuristic considerations, others are not.
Cite as

Michael Stoll. Rational Points on Curves of Genus 2: Experiments and Speculations. In Algorithms and Number Theory. Dagstuhl Seminar Proceedings, Volume 9221, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{stoll:DagSemProc.09221.5,
  author =	{Stoll, Michael},
  title =	{{Rational Points on Curves of Genus 2: Experiments and Speculations}},
  booktitle =	{Algorithms and Number Theory},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9221},
  editor =	{Johannes A. Buchmann and John Cremona and Michael E. Pohst},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09221.5},
  URN =		{urn:nbn:de:0030-drops-21246},
  doi =		{10.4230/DagSemProc.09221.5},
  annote =	{Keywords: Rational points, genus 2}
}
  • Refine by Author
  • 1 Angdinata, David Kurniadi
  • 1 Stoll, Michael
  • 1 Xu, Junyan

  • Refine by Classification
  • 1 Mathematics of computing → Mathematical software
  • 1 Security and privacy → Logic and verification
  • 1 Theory of computation → Interactive proof systems

  • Refine by Keyword
  • 1 Lean
  • 1 Rational points
  • 1 algebraic geometry
  • 1 elliptic curve
  • 1 formal math
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2009
  • 1 2023

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