一句话：在 Coq 中完成 DPRM 定理的首次完整机器化证明，形式化了希尔伯特第十问题的不可判定性。
本文在 Coq 构造型类型论中形式化丢番图方程可解性的不可判定性，即希尔伯特第十问题。作者首次完整机器化证明 Davis-Putnam-Robinson-Matiyasevich 定理：每个递归可枚举问题（文中用 Minsky 机表示）都是丢番图的。证明采用合成可计算性方法，并引入 Conway 的 FRACTRAN 语言作为中间层，使证明更简洁易懂。文章还证明反向方向：每个丢番图关系可由 μ-递归函数识别，并给出从 μ-递归函数到 Minsky 机的已验证编译器。关键结果是获得 DPRM 定理及其推论在 Coq 中的完整形式化。
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.
@article{paperbot1718,
title = {Hilbert's Tenth Problem in Coq (Extended Version)},
author = {Dominique Larchey-Wendling and Yannick Forster},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:35)2022}
}