Papers With

← All papers
First page of 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

David Kurniadi Angdinata, Junyan Xu

cs.LO Feb 21, 2023 · v1
formalization mathlib number-theory algebra
Read PDF arXiv abstract
TL;DR
Formalizes in Lean that nonsingular points of a Weierstrass elliptic curve form an abelian group.
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 of associativity involve either advanced algebraic geometry or tedious computation, especially in characteristic two. The authors 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.
Problem

Formal proofs of associativity for the group law on elliptic curves either require advanced algebraic geometry (schemes, divisors) or tedious computation, especially in characteristic two where standard simplifications fail.

Approach

The authors formalize in Lean the type of nonsingular points of a Weierstrass curve over a field of any characteristic and provide a purely algebraic proof that it forms an abelian group. The approach avoids advanced algebraic geometry by working directly with the Weierstrass equation, handling all characteristics uniformly including the problematic characteristic-two case.

Results

The formalization produces a complete machine-checked proof of the group law on Weierstrass elliptic curves valid in any characteristic, eliminating the need for case splits on the field characteristic or appeals to scheme-theoretic arguments.