University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean

Download to your calendar using vCal

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki .

I’ll discuss some recent work on defining modular forms and Eisenstein series in LEAN . Modular forms are some of the most important objects in number theory due in part to their role in the proof of Fermat’s Last Theorem. These special functions act as glue between algebra, geometry and analysis, it is therefore tempting to begin formalizing them. Moreover one wants to formalise interesting examples, such as Eisenstein series. In the talk I will discuss the mathematics behind there definitions and highlight the main challenges in formalising them.

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

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Cambridge & County Folk Museum, Castle Street MRL meeting rooms 1 & 2, Level 4 Institute of Metabolic Sciences, Addenbrooke’s Treatment Centre (ATC) Sir David King's Surface Science Seminars

Other talks

Teams Announced Tea and Coffee Break FILM: One With The Whale Discussion II continued Online Causal Inference Seminar Title TBC
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity