Abstract

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