BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Structures in dependent type theory - Professor Jeremy Avigad (Car
 negie Mellon University)
DTSTART:20240215T170000Z
DTEND:20240215T180000Z
UID:TALK210391@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Reasoning about axiomatically characterized abstract structure
 s has been central to mathematics since the early twentieth century. The a
 bility of Lean and its mathematical library\, Mathlib\, to manage a comple
 x network of such structures has been essential to their acceptance by the
  mathematical community. In this talk\, I will discuss some of the challen
 ges that structural reasoning brings and how they are addressed in Lean an
 d Mathlib. I will also discuss recent work by Joshua Clune\, Yicheng Qian\
 , and Alexander Bentkamp toward developing automated reasoning tools that 
 work in such an environment.\n\n---\n\nWATCH ONLINE HERE : https://www.mic
 rosoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 
 279 261 Passcode: iCo7a5
LOCATION:Live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR