Little theories for big formal proofs

Add to your list(s) Download to your calendar using vCal

• Georges Gonthier (Inria)
• Thursday 23 May 2024, 17:00-18:00
• Live-streamed at MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

The growing practice of using proof assistant software to create and mechanically check formal proofs of challenging mathematical results relies crucially on the prior formalisation of their elementary prerequisites. These include both common undergraduate material and mundane, essentially trivial facts about symbol manipulation. The feasibility of bigger proofs depends, sometimes critically, on how one has chosen to formalise these « little theories ». This talk will explore some instances of such dependencies, drawn from my experience in formalising the proofs of the Four Colour and Odd Order theorems.

——-

This talk will be streamed online via Zoom.

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89458346264?pwd=Wkt2NUNwV0xzTGkyR2hGQUVGRThsUT09

Meeting ID: 894 5834 6264 Passcode: 738052

—-

One tap mobile +441314601196,,89458346264#,,,,738052# United Kingdom +442034815237,,89458346264#,,,,738052# United Kingdom

—-

Dial by your location • +44 131 460 1196 United Kingdom • +44 203 481 5237 United Kingdom • +44 203 481 5240 United Kingdom • +44 203 901 7895 United Kingdom • +44 208 080 6591 United Kingdom • +44 208 080 6592 United Kingdom • +44 330 088 5830 United Kingdom

Meeting ID: 894 5834 6264 Passcode: 738052

Find your local number: https://cam-ac-uk.zoom.us/u/kcKW3mcRjF

—-

Join by SIP • 89458346264@zoomcrc.com

—-

Join by H.323 • 162.255.37.11 (US West) • 162.255.36.11 (US East) • 115.114.131.7 (India Mumbai) • 115.114.115.7 (India Hyderabad) • 213.19.144.110 (Amsterdam Netherlands) • 213.244.140.110 (Germany) • 103.122.166.55 (Australia Sydney) • 103.122.167.55 (Australia Melbourne) • 149.137.40.110 (Singapore) • 64.211.144.160 (Brazil) • 149.137.68.253 (Mexico) • 69.174.57.160 (Canada Toronto) • 65.39.152.160 (Canada Vancouver) • 207.226.132.110 (Japan Tokyo) • 149.137.24.110 (Japan Osaka)

Meeting ID: 894 5834 6264 Passcode: 738052

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• Live-streamed at MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.