University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > New Foundations: the story of a large formalisation project

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

New Foundations: the story of a large formalisation project

Download to your calendar using vCal

If you have a question about this talk, please contact Anand Rao Tadipatri .

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 ===

Recording: https://www.youtube.com/watch?v=2MBe6minTfE

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

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Alison Richard Building, Sidgwick Site, Seminar Room SG1 Main Physiology Lecture Theatre (Theatre 1), Physiology Department, Downing Site FAMES, Common Room

Other talks

Haematology and Palliative Care Title to be confirmed Paediatric Medicine and Rheumatology Morning Break Emergency Medicine and Metabolic Medicine Topology of the Ritz energy landscape
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity