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

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

• Chris Birkbeck (University College London)
• Tuesday 01 November 2022, 14:30-15:30
• Centre for Mathematical Sciences, MR13.

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:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Centre for Mathematical Sciences, MR13
• DPMMS Lists
• DPMMS Pure Maths Seminar
• DPMMS info aggregator
• DPMMS lists
• Hanchen DaDaDash
• Interested Talks
• Number Theory Seminar
• School of Physical Sciences
• bld31

Note that ex-directory lists are not shown.