University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > 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 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.

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