Diophantine Equations and the DPRM Theorem

Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri Matiyasevich and Dierk Schleicher

June 6, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session DPRM_Theorem