BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalising modular forms\, Eisenstein series and the statement of
  the modularity conjecture in Lean - Dr Chris Birkbeck (University of East
  Anglia)
DTSTART:20230427T160000Z
DTEND:20230427T170000Z
UID:TALK196699@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:I’ll discuss some recent work on defining modular forms and 
 Eisenstein series in LEAN. Modular forms are some of the most important ob
 jects 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\, geom
 etry and analysis\, it is therefore tempting to begin formalizing them. Mo
 reover one wants to formalise interesting examples\, such as Eisenstein se
 ries. In the talk I will discuss the mathematics behind there definitions 
 and highlight the main challenges in formalising them.\n\n\n
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR