Email Gateway (Jun 07 2022 at 11:40): Email Gateway (Jun 07 2022 at 11:40):From: Lawrence Paulson <lp15@cam.ac.uk>
This long awaited entry is finally here!
We present a formalization of Matiyasevich's proof of the DPRM theorem, which states that every recursively enumerable set of natural numbers is Diophantine. This result from 1970 yields a negative solution to Hilbert's 10th problem over the integers. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. We formalize a general theory of Diophantine sets and relations to reason about them abstractly. Using several number-theoretic lemmas, we prove that exponentiation has a Diophantine representation.
Many thanks to Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri Matiyasevich and Dierk Schleicher for this substantial and deeply impressive development. You will find it here:
https://www.isa-afp.org/entries/DPRM_Theorem.html
Larry
Last updated: Jan 04 2025 at 20:18 UTC