University of Cambridge > > Wednesday Seminars - Department of Computer Science and Technology  > Formalised Mathematics: Obstacles and Achievements

Formalised Mathematics: Obstacles and Achievements

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

If you have a question about this talk, please contact Ben Karniely.

The practice of formalising mathematics is starting to attract the attention of mathematicians themselves. The main motivation is an awareness that mathematicians regularly make serious errors, some of which go undetected. But is formalised mathematics at all a realistic possibility? By now a great body of mathematics has been formalised. Unfortunately, rather little of it approaches the sophistication of modern research mathematics. Moreover, formalised proofs are typically unreadable and require lengthy blocks of code to prove obvious facts. Researchers are now formalising more advanced mathematical concepts, but much more remains to be done.

Link to join virtually:

A recording of this talk is available at the following link:

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology 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