Universal Diophantine Equations in Isabelle

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

• Jonas Bayer (University of Cambridge)
• Thursday 29 May 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

If you have a question about this talk, please contact Anand Rao Tadipatri.

Abstract: In this talk I will present the formalisation of a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalisation of my own work in number theory.

Hilbert’s Tenth Problem (H10) was answered negatively by Yuri Matiyasevich, who showed that there is no general algorithm to decide whether an arbitrary Diophantine equation has a solution. I will give an introduction to Hilbert’s Problem and its original solution. Moreover, I will motivate and give the key idea of the stronger version of H10 which we formalised. Finally, I will talk about the various challenges that came up during the formalisation and, more importantly, the insights we drew from formalising our yet-unpublished, unpolished manuscript.

This is joint work with Marco David, Timothé Ringeard, Xavier Pigé, Anna Danilkin, Mathis Bouverot-Dupuis, Paul Wang, Quentin Vermande, Theo Andrée, Loïc Chevalier, Charlotte Dorneich, Eva Brenner, Chris Ye, Kevin Lee, Malte Haßler, Simon Dubischar, Thomas Serafini, Dierk Schleicher and Yuri Matiyasevich.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

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

This talk is included in these lists:

• 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
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.