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.

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