Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Diophantine Equations and the ...


view this post on Zulip 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: Jul 15 2022 at 23:21 UTC