BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Integrating Formal and Informal Reasoning - Chase Norman (Carnegie
  Mellon University)
DTSTART:20251204T170000Z
DTEND:20251204T180000Z
UID:TALK240103@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:What is the proper interface for an informal reasoner to engag
 e in formal proof? In this talk\, I will delineate a precise boundary in r
 esponsibilities between deductive procedures and informal intuition. With 
 this\, I will showcase a vision for a future-proof interface that plays to
  the strengths of each\, without overburdening either. This allows for dee
 p integration of machine learning methods with proof assistants\, and reve
 als aspects of the nature of mathematics itself.\n\n=== Online talk ===\n\
 nJoin Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuT
 ideTlH6PjAmbXLO8HbY.1\n\nMeeting ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:Centre for Mathematical Sciences\, MR14
END:VEVENT
END:VCALENDAR