Formalised Mathematics: Obstacles and Achievements

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

• Professor Lawrence C. Paulson FRS (University of Cambridge)
• Thursday 19 January 2023, 17:00-18:00
• Centre for Mathematical Sciences MR12, CMS.

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki.

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.

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• Centre for Mathematical Sciences MR12, CMS
• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.