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

TL;DR

This paper provides a formal, elementary proof in Lean that the set of nonsingular points on a Weierstrass elliptic curve forms an abelian group, valid in any characteristic, avoiding complex geometric or computational methods.

Contribution

It offers the first elementary formal proof of the group law's associativity on Weierstrass elliptic curves in any characteristic within a proof assistant.

Findings

Formal proof in Lean confirms the group law is associative for all characteristics.

The proof is purely algebraic, avoiding advanced geometric or computational techniques.

Applicable to all nonsingular points on Weierstrass elliptic curves over any field.

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.