BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Prospects for formalizing the theory of weak infinite-dimensional 
 categories - Emily Riehl (Johns Hopkins University)
DTSTART:20250130T170000Z
DTEND:20250130T180000Z
UID:TALK224938@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:A peculiarity of the ∞-categories literature is that proofs 
 are often written without reference to a concrete definition of an ∞-cat
 egory\, a practice that creates an impediment to formalization. We describ
 e three broad strategies that would make ∞-category theory formalizable\
 , which may be described as “analytic\,” “axiomatic\,” and “synt
 hetic.” We then highlight two parallel ongoing collaborative efforts to 
 formalize ∞-category theory in two different proof assistants: the “ax
 iomatic” theory in Lean and the “synthetic” theory in Rzk. We show s
 ome sample formalized proofs to highlight the advantages and drawbacks of 
 each approach and explain how you could contribute to this effort. This in
 volves joint work with Mario Carneiro\, Nikolai Kudasov\, Dominic Verity\,
  Jonathan Weinberger\, and many others.\n\n=== Online talk ===\n\nJoin Zoo
 m Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCs
 booOVqenzI.1\n\nMeeting ID: 871 4336 5195\n\nPasscode: 541180
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR