Formalised Mathematics: Obstacles and Achievements
- đ¤ Speaker: Professor Lawrence Paulson - Department of Computer Science and Technology
- đ Date & Time: Wednesday 23 November 2022, 15:05 - 15:55
- đ Venue: Lecture Theatre 1, Computer Laboratory, William Gates Building
Abstract
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/
Series This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Chris Davis' list
- computer science
- 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
- se393's list
- Trust & Technology Initiative - interesting events
- Wednesday Seminars - Department of Computer Science and Technology
- yk449
Note: Ex-directory lists are not shown.
![[Talks.cam]](/static/images/talkslogosmall.gif)

Professor Lawrence Paulson - Department of Computer Science and Technology
Wednesday 23 November 2022, 15:05-15:55