How Hilbert met Isabelle: Proof Between Generations

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

• Marco David (École Normale Supérieure de Paris)
• Thursday 26 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.

Hybrid talk (please see abstract for link)

In late 2017, a group of then first-year students started formalizing the mathematics around Hilbert’s Tenth Problem with Isabelle. A pilot project in many ways, we learned how to use proof assistants for learning mathematics and for doing contemporary research, in constant interaction with the computer. Five years later, we will look back on this intergenerational work, the lessons learned, and give an outlook on new opportunities.

WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 379 992 884 209 Passcode: TYR8 Sh

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.