Formalised Mathematics: Obstacles and Achievements

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

• Professor Lawrence Paulson - Department of Computer Science and Technology
• Wednesday 23 November 2022, 15:05-15:55
• Lecture Theatre 1, Computer Laboratory, William Gates Building.

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: https://zoom.us/j/98901725392?pwd=UWNVZVFTcVQxL2JkS0V1WVBoelBuUT09

A recording of this talk is available at the following link: https://www.cl.cam.ac.uk/seminars/wednesday/video/

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory, William Gates Building
• Martin's interesting talks
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list
• yk449

Note that ex-directory lists are not shown.