Modular forms and Eisenstein series

Abstract: 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.

general mathematicsnumber theory

Audience: advanced learners

Comments: This talk will be a Zoom talk. I (Kevin Buzzard) am not in London this week so I will not be running the show in the usual room, and do not know if anyone will be there to run it because I was too disorganised to sort anything out before I left London. See you on Zoom!

---

London Learning Lean

Series comments: This is a seminar on formalising research level, MSc, or advanced undergraduate level mathematics in the Lean theorem prover. It is suitable for people who have some mathematical background, e.g. MSc students in a mathematics department. Speakers will assume some familiarity with the Lean but you certainly don't have to be a Lean expert

Speakers are told to spend 50 percent of their time explaining the mathematics, and 50 percent on the Lean implementation.

Past seminars are available on the YouTube playlist here www.youtube.com/watch?v=UykGFDVfQNA&list=PLVZep5wTamMmqv34JnrNC2AgjfPoh_LN8

The seminar series is hybrid/online -- it will meet in person at Imperial College in room Huxley 410, and will also be live streamed on Zoom.

---