An elementary proof of the group law for elliptic curves (Q1676248)

The author presents a computational (formal) proof of the existence of a group structure for an elliptic curve \(E:y^2=x^3+ax+b\) (i.e., basically, of the associativity of the group law). The various cases for the equality \(A+(B+C)=(A+B)+C\) (i.e., \(A=B\), \(A+B=C\), etc...) are treated separately and explicitly: many of them require long and hard computations which were performed using the algebraic computational system CoCoA.