University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > How Hilbert met Isabelle: Proof Between Generations

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹ️ Information

How Hilbert met Isabelle: Proof Between Generations

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

CCLP Online: https://teams.microsoft.com/l/meetup-join/19%3ameeting_MDIzZDBmNDEtNTZlNC00MzFkLWEzNWEtODBmZmI5NWE0NzJh%40thread.v2/0?context=%7b%22Tid%22%3a%2249a50445-bdfa-4b79-ade3-547b4f3986e9%22%2c%22Oid%22%3a%2215d66985-4ebf-4bf2-a70f-da9a8a459e44%22%7d Rooms SG1 & SG2, Alison Richard Building, 7 West Road, Cambridge, CB3 9DT

Other talks

When Programmes Disagree About Programmes: Code Poetry and the Problem of Programme–Programme Communication Tea and Coffee Break Title to be confirmed Group Presentation 3 TBC Title to be confirmed
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity