We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq's constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem -- in our case by a Minsky machine -- is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway's FRACTRAN language as intermediate layer. Additionally, we prove the reverse direction and show that every Diophantine relation is recognisable by $\mu$-recursive functions and give a certified compiler from $\mu$-recursive functions to Minsky machines.

翻译：我们按照Coq的建设性类型理论,将diophanantine 等式(即相对于自然数字的多式方程式)的可溶性正式确定为不可溶性。 为此,我们首次将Davis-Putnam-Robinson-Matiyasevich 理论完全机械化,指出每一个可反复出现的问题 -- -- 就我们而言,由明斯克机器 -- -- 都属于Diophantine。我们通过使用合成方法来兼容性并采用Conway的FRACTRAN语言作为中间层,获得了优雅和易懂的证据。此外,我们证明了反向方向,并表明每一种diophanine关系都可以被 $-mu$-recurective 函数识别,并向明斯克机器提供由$\mu$-recurive函数组成的经认证的编译器。