I will present in this talk some insights about the formalization of mathematics, using the case study of a formal development of some elliptic curves theory in the coq proof assistant

The theory of elliptic curves is a subject where one finds diverse branches of mathematics, such as, complex analysis, algebraic geometry, representation theory and number theory. It has been an active field of study since the 19th century. Elliptic curves have been used to approach a wide range of problems such as the fast factorisation of integers and the search for congruent numbers. In the 20th century, they have regained interest because of their applications in cryptography, first suggested in 1985 independently by Neal Koblitz and Victor Miller. Elliptic curve theory remains a subject of active research because of its wide range of applications, as well as the rich mathematics behind it.