Algebraising foundations of elliptic curves

Elliptic curves are one of the simplest non-trivial objects in algebraic geometry, which are pervasive in modern number theory, but also see applications in point counting algorithms and public key cryptography. Due to their geometric nature, formalising a working definition typically requires a lot of technical machinery, let alone any non-trivial results. Yet, the Lean community has managed to formalise two of the most fundamental theorems in the theory of elliptic curves, with scope for many more projects. In this talk, I will explain these theorems, and how we inadvertently discovered new proofs in our formalisation attempts.

Slides: https://multramate.github.io/talks/afoec/main.pdf