![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Thursday 19 January 2023, 17:00-18:00
Formalised Mathematics: Obstacles and Achievements
- đ¤ Speaker: Professor Lawrence C. Paulson FRS (University of Cambridge) đ Website
- đ Date & Time: Thursday 19 January 2023, 17:00 - 18:00
- đ Venue: Centre for Mathematical Sciences MR12, CMS
Questions? Contact
Angeliki Koutsoukou-Argyraki
Abstract
Interest in doing mathematics by computer dates back to the 1950s. The talk will survey work on the mechanisation of mathematics by both interactive and automatic means up to the present day. Then it will focus in more detail on some of the latest achievements done in Isabelle/HOL and Lean, concluding with remarks on the research issues that still need to be overcome.
Series This talk is part of the Formalisation of mathematics with interactive theorem provers series.
Included in Lists
- All CMS events
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Centre for Mathematical Sciences MR12, CMS
- CMS Events
- Department of Computer Science and Technology talks and seminars
- DPMMS info aggregator
- DPMMS lists
- DPMMS Lists
- DPMMS Pure Maths study groups
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- Martin's interesting talks
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.