Download PDFOpen PDF in browser

Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle

EasyChair Preprint no. 152

11 pagesPublished: May 22, 2018


Hilbert's tenth problem, posed in 1900 by David Hilbert, asks for a general algorithm to determine the solvability of any given Diophantine equation. In 1970, Yuri Matiyasevich proved the DPRM theorem which implies such an algorithm cannot exist. This paper will outline our attempt to formally state the DPRM theorem and verify Matiyasevich's proof using the proof assistant Isabelle/HOL.

Keyphrases: Diophantine equations, DPRM Theorem, Hilbert's tenth problem, Isabelle, recursively enumerable

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Benedikt Stock and Abhik Pal and Maria Antonia Oprea and Yufei Liu and Malte Sophian Hassler and Simon Dubischar and Prabhat Devkota and Yiping Deng and Marco David and Bogdan Ciurezu and Jonas Bayer and Deepak Aryal},
  title = {Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle},
  howpublished = {EasyChair Preprint no. 152},
  doi = {10.29007/3q4s},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser