تقرير
An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic
| العنوان: | An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in any Characteristic |
|---|---|
| المؤلفون: | Angdinata, David Kurniadi, Xu, Junyan |
| سنة النشر: | 2023 |
| المجموعة: | Computer Science Mathematics |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science, Mathematics - Commutative Algebra, Mathematics - Algebraic Geometry, Mathematics - Number Theory, 14H52, 68V20, F.4.1, G.4 |
| الوصف: | 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. Comment: Submitted to 14th International Conference on Interactive Theorem Proving (ITP 2023), source code in https://github.com/alreadydone/mathlib/tree/associativity |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2302.10640 |
| رقم الأكسشن: | edsarx.2302.10640 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |