Algebraising foundations of elliptic curves

Add to your list(s) Download to your calendar using vCal

• David Angdinata (University College London)
• Thursday 13 February 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.