BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Little theories for big formal proofs - Professor Georges Gonthier
  (Inria)
DTSTART:20240523T160000Z
DTEND:20240523T170000Z
UID:TALK216109@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:The growing practice of using proof assistant software to crea
 te and mechanically check formal proofs of challenging mathematical result
 s relies crucially on the prior formalisation of their elementary prerequi
 sites. These include both common undergraduate material and mundane\, esse
 ntially trivial facts about symbol manipulation. The feasibility of bigger
  proofs depends\, sometimes critically\, on how one has chosen to formalis
 e these « little theories ». This talk will explore some instances of su
 ch dependencies\, drawn from my experience in formalising the proofs of th
 e Four Colour and Odd Order theorems.\n\n-----\n\nThis talk will be stream
 ed online via Zoom.\n\nJoin Zoom Meeting\nhttps://cam-ac-uk.zoom.us/j/8945
 8346264?pwd=Wkt2NUNwV0xzTGkyR2hGQUVGRThsUT09\n\nMeeting ID: 894 5834 6264\
 nPasscode: 738052\n\n---\n\nOne tap mobile\n+441314601196\,\,89458346264#\
 ,\,\,\,*738052# United Kingdom\n+442034815237\,\,89458346264#\,\,\,\,*7380
 52# United Kingdom\n\n---\n\nDial by your location\n• +44 131 460 1196 U
 nited Kingdom\n• +44 203 481 5237 United Kingdom\n• +44 203 481 5240 U
 nited Kingdom\n• +44 203 901 7895 United Kingdom\n• +44 208 080 6591 U
 nited Kingdom\n• +44 208 080 6592 United Kingdom\n• +44 330 088 5830 U
 nited Kingdom\n\nMeeting ID: 894 5834 6264\nPasscode: 738052\n\nFind your 
 local number: https://cam-ac-uk.zoom.us/u/kcKW3mcRjF\n\n---\n\nJoin by SIP
 \n• 89458346264@zoomcrc.com\n\n---\n\nJoin by H.323\n• 162.255.37.11 (
 US West)\n• 162.255.36.11 (US East)\n• 115.114.131.7 (India Mumbai)\n
 • 115.114.115.7 (India Hyderabad)\n• 213.19.144.110 (Amsterdam Netherl
 ands)\n• 213.244.140.110 (Germany)\n• 103.122.166.55 (Australia Sydney
 )\n• 103.122.167.55 (Australia Melbourne)\n• 149.137.40.110 (Singapore
 )\n• 64.211.144.160 (Brazil)\n• 149.137.68.253 (Mexico)\n• 69.174.57
 .160 (Canada Toronto)\n• 65.39.152.160 (Canada Vancouver)\n• 207.226.1
 32.110 (Japan Tokyo)\n• 149.137.24.110 (Japan Osaka)\n\nMeeting ID: 894 
 5834 6264\nPasscode: 738052
LOCATION:Live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR