University of Cambridge > Talks.cam > Number Theory Seminar > Formalising modular forms, Eisenstein series and the modularity conjecture in Lean

  Browse A-Z

Log in

University Account External (via Google)

🔐 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 modularity conjecture in Lean

Download to your calendar using vCal

If you have a question about this talk, please contact Rong Zhou .

I’ll discuss some recent work on defining modular forms and Eisenstein series in Lean. This is an interactive theorem prover which has recently attracted mathematicians and computer scientists who are working together to create a unified digitised library of mathematics. In my talk I will explain what Lean is and explain the process of taking basic definitions/examples of modular forms and formalising them.

This talk is part of the Number Theory Seminar series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

FW11, William Gates Building. Zoom link: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon Webinar & FW11, Computer Laboratory, William Gates Building. Average on weekdays: 8921.50690335 kWh

Other talks

Cooperation for Nature Spectral rigidity of random covers of compact hyperbolic surfaces Title TBC Title to be confirmed External Seminar - Hilde Nelissen TBC Synthesizing Diverse Policies for Multi-Agent Coordination
 

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