In this talk, I will discuss the experiences and challenges of running a successful formalisation project: proving the consistency of Quine’s set theory New Foundations. The main focus will be on the interesting and unexpected ways in which large formalisation projects differ from small ones, and how we can use formalisation to get better at ‘paper’ mathematics.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180