BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Chris Birkbeck (University College London)
DTSTART:20220120T160000Z
DTEND:20220120T170000Z
DTSTAMP:20260414T152148Z
UID:LondonLearningLean/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LondonLearni
 ngLean/2/">Modular forms  and Eisenstein series</a>\nby Chris Birkbeck (Un
 iversity College London) as part of London Learning Lean\n\n\nAbstract\nI
 ’ll discuss some recent work on defining modular forms and Eisenstein se
 ries in LEAN. Modular forms are some of the most important objects in numb
 er theory due in part to their role in the proof of Fermat’s Last Theore
 m.  These special functions act as glue between algebra\, geometry and ana
 lysis\, it is therefore tempting to begin formalizing them. Moreover one w
 ants to formalise interesting examples\, such as Eisenstein series. In the
  talk I will discuss the mathematics behind there definitions and highligh
 t the main challenges in formalising them.\n\nThis talk will be a Zoom tal
 k. I (Kevin Buzzard) am not in London this week so I will not be running t
 he 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 Lond
 on. See you on Zoom!\n
LOCATION:https://researchseminars.org/talk/LondonLearningLean/2/
END:VEVENT
END:VCALENDAR