Download PDFOpen PDF in browserHilbert Meets Isabelle: Formalisation of the DPRM Theorem in IsabelleEasyChair Preprint 15211 pages•Date: May 22, 2018AbstractHilbert'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: DPRM Theorem, Diophantine equations, Hilbert's tenth problem, Isabelle, recursively enumerable
|