BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalizing invisible mathematics: case studies from higher catego
 ry theory - Emily Riehl (Johns Hopkins University)
DTSTART:20250609T104500Z
DTEND:20250609T114500Z
UID:TALK230662@talks.cam.ac.uk
DESCRIPTION:One thing that quickly becomes clear when attempting to formal
 ize recent mathematical discoveries in a computer proof assistant is how m
 uch "invisible mathematics" is obscured in a proof on paper. This talk wil
 l attempt to present a taxonomy of the various forms of invisible mathemat
 ics that have been made visible by attempts to formalize higher category t
 heory. We then describe specific challenges inherent to large-scale formal
 ization projects that are exacerbated by invisible mathematics.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR