BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Liquid Tensor Experiment - Professor Kevin Buzzard (Imperial C
 ollege London)
DTSTART:20230202T170000Z
DTEND:20230202T180000Z
UID:TALK192551@talks.cam.ac.uk
CONTACT:Angeliki Koutsoukou-Argyraki
DESCRIPTION:In July 2022 a team led by Johan Commelin and Adam Topaz compl
 etely formalised in Lean the proof of a theorem of Dustin Clausen and Pete
 r Scholze. Scholze described the result by saying "I think this may be my 
 most important theorem to date". What is the point of formalising it\, wha
 t did it teach us\, and what happens next?
LOCATION:  Centre for Mathematical Sciences MR12\, CMS
END:VEVENT
END:VCALENDAR