BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
rem provers
SUMMARY:Formalising modular forms\, Eisenstein series and
the statement of the modularity conjecture in Lean
- Dr Chris Birkbeck (University of East Anglia)
DTSTART;TZID=Europe/London:20230427T170000
DTEND;TZID=Europe/London:20230427T180000
UID:TALK196699AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/196699
DESCRIPTION: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 F
ermat’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 exam
ples\, such as Eisenstein series. In the talk I wi
ll discuss the mathematics behind there definition
s and highlight the main challenges in formalising
them.\n\n\n
LOCATION: Centre for Mathematical Sciences MR12\, CMS
CONTACT:Angeliki Koutsoukou-Argyraki
END:VEVENT
END:VCALENDAR