University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > Little theories for big formal proofs

Little theories for big formal proofs

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

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 is part of the Formalisation of mathematics with interactive theorem provers series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


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