BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Universal Diophantine Equations in Isabelle - Jonas Bayer (Univers
 ity of Cambridge)
DTSTART:20250529T160000Z
DTEND:20250529T170000Z
UID:TALK232426@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:If you have a question about this talk\, please contact Anand 
 Rao Tadipatri.\n\nAbstract:\nIn this talk I will present the formalisation
  of a universal construction of Diophantine equations with bounded complex
 ity in Isabelle/HOL. This is a formalisation of my own work in number theo
 ry.\n\nHilbert's Tenth Problem (H10) was answered negatively by Yuri Matiy
 asevich\, who showed that there is no general algorithm to decide whether 
 an arbitrary Diophantine equation has a solution. I will give an introduct
 ion to Hilbert’s Problem and its original solution. Moreover\, I will mo
 tivate and give the key idea of the stronger version of H10 which we forma
 lised. Finally\, I will talk about the various challenges that came up dur
 ing the formalisation and\, more importantly\, the insights we drew from f
 ormalising our yet-unpublished\, unpolished manuscript. \n\nThis 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 Y
 uri Matiyasevich.\n\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting https://ca
 m-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1\n\nMeet
 ing ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR