BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Certifying Synthetic Mathematics in Lean - Wojciech Nawrocki (Carn
 egie Mellon University)
DTSTART:20260219T170000Z
DTEND:20260219T180000Z
UID:TALK243274@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Synthetic theories such as homotopy type theory axiomatize cla
 ssical mathematical objects such as spaces up to homotopy. Although theore
 ms in synthetic theories translate to theorems about the axiomatized struc
 tures on paper\, this fact has not yet been exploited in proof assistants.
  This makes it challenging to formalize results in classical mathematics u
 sing synthetic methods. For example\, Cubical Agda supports reasoning abou
 t cubical types\, but cubical proofs have not been translated to proofs ab
 out cubical set models\, let alone their topological realizations.\n\nIn t
 his talk we will present SynthLean: a proof assistant that fills this gap 
 by combining reasoning using synthetic theories with reasoning about their
  models.\n\nSynthLean is part of the HoTTLean project\, presented by Steve
  Awodey in this seminar series a week prior (on February 12th).\n\n=== Onl
 ine talk ===\n\nJoin Zoom 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
END:VEVENT
END:VCALENDAR