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 they form an abelian group.

翻译：椭圆曲线是数论与代数几何中的基本对象，其域上点在几何加法法则下构成阿贝尔群。域上任意椭圆曲线均具有Weierstrass模型，但先前关于该模型中加法结合律的形式化证明要么涉及高等代数几何，要么需要繁琐计算——尤其在特征为2的情形下。我们在Lean定理证明器中形式化了任意特征域上Weierstrass曲线的非奇异点类型，并给出一个纯代数证明，证实这些点构成阿贝尔群。