BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Formalisation of mathematics with interactive theo
 rem provers 
SUMMARY:Certifying Synthetic Mathematics in Lean - Wojciec
 h Nawrocki (Carnegie Mellon University)
DTSTART;TZID=Europe/London:20260219T170000
DTEND;TZID=Europe/London:20260219T180000
UID:TALK243274AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/243274
DESCRIPTION:Synthetic theories such as homotopy type theory ax
 iomatize classical mathematical objects such as sp
 aces up to homotopy. Although theorems in syntheti
 c theories translate to theorems about the axiomat
 ized structures on paper\, this fact has not yet b
 een exploited in proof assistants. This makes it c
 hallenging to formalize results in classical mathe
 matics using synthetic methods. For example\, Cubi
 cal Agda supports reasoning about cubical types\, 
 but cubical proofs have not been translated to pro
 ofs about cubical set models\, let alone their top
 ological realizations.\n\nIn this talk we will pre
 sent SynthLean: a proof assistant that fills this 
 gap by combining reasoning using synthetic theorie
 s with reasoning about their models.\n\nSynthLean 
 is part of the HoTTLean project\, presented by Ste
 ve Awodey in this seminar series a week prior (on 
 February 12th).\n\n=== Online talk ===\n\nJoin Zoo
 m Meeting https://cam-ac-uk.zoom.us/j/89856091954?
 pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeeting ID
 : 898 5609 1954 Passcode: ITPtalk\n\n
LOCATION:MR14 Centre for Mathematical Sciences
CONTACT:Anand Rao Tadipatri
END:VEVENT
END:VCALENDAR