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 modularity c
 onjecture in Lean - Chris Birkbeck (University College London)
DTSTART:20221101T143000Z
DTEND:20221101T153000Z
UID:TALK180410@talks.cam.ac.uk
CONTACT:Rong Zhou
DESCRIPTION:I’ll discuss some recent work on defining modular forms and 
 Eisenstein series in Lean. This is an interactive theorem prover which has
  recently attracted mathematicians and computer scientists who are working
  together to create a unified digitised library of mathematics. In my talk
  I will explain what Lean is and explain the process of taking basic defin
 itions/examples of modular forms and formalising them.
LOCATION:Centre for Mathematical Sciences\, MR13
END:VEVENT
END:VCALENDAR