希尔伯特第十问题在 Coq 中的形式化（扩展版）
Hilbert's Tenth Problem in Coq (Extended Version)
AI总结：
本文在 Coq 中形式化丢番图方程可解性的不可判定性，首次完整机械化 DPRM 定理，并通过 FRACTRAN 中间层获得优雅证明，同时证明反向方向并给出 μ-递归函数到 Minsky 机的认证编译器。
摘要：
我们在 Coq 的构造性类型理论中形式化了丢番图方程（即自然数上的多项式方程）可解性的不可判定性。为此，我们首次完整机械化 Davis-Putnam-Robinson-Matiyasevich 定理，该定理断言每个递归可枚举问题（在我们的情形中由 Minsky 机给出）都是丢番图的。通过采用可计算性的综合方法，并引入 Conway 的 FRACTRAN 语言作为中间层，我们获得了一个优雅且易于理解的证明。此外，我们证明了反向方向，表明每个丢番图关系都可被 μ-递归函数识别，并给出了从 μ-递归函数到 Minsky 机的经过认证的编译器。
英文摘要：
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 $μ$-recursive functions and give a certified compiler from $μ$-recursive functions to Minsky machines.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
