skip to content

Department of Computer Science and Technology

Thursday, 27 April, 2023 - 17:00 to 18:00
Dr Chris Birkbeck (University of East Anglia)
Centre for Mathematical Sciences MR12, CMS

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.

Seminar series: 
Formalisation of mathematics with interactive theorem provers

Upcoming seminars