2026-07-21T14:16:29Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10534 2024-03-06T10:46:09Z ddc:004 open_access

Hilbert’s Tenth Problem in Coq Larchey-Wendling, Dominique Forster, Yannick Hilbert’s tenth problem Diophantine equations undecidability computability theory reduction Minsky machines Fractran Coq type theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dominique Larchey-Wendling and Yannick Forster 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.27 urn:nbn:de:0030-drops-105342 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.27 eng https://creativecommons.org/licenses/by/3.0/legalcode