In 1900, at the International Congress of Mathematicians in Paris and in a publication that shortly followed, David Hilbert presented the twenty-three most important problems for the coming century. The tenth problem concerns the solvability of Diophantine equations and was resolved in 1970 by Yuri Matiyasevich (DPRM theorem).

We conduct a formal verification of Matiyasevich's original proof using the proof assistant Isabelle. We formally state each lemma in Isabelle's formal language and prove each required step. The complete formalised proof includes even the simplest details such as commutativity of matrix addition and more abstract concepts like termination of register machines. At the time of writing, we have completely formalised the proof that exponentiation is Diophantine --- Matiyasevich's key breakthrough from 1970. We have also produced a model of a register machine and shown that given equations describing a certain register machine we can encode them as geometric sums (and hence, as exponential Diophantine equations). Additional work will produce proofs that simulate a register machine as equations. This will then result in a full formalisation of the DPRM theorem.

Fourteen of the original Hilbert problems have been resolved and none of the solutions have been formally verified yet. Our project will be the first complete such formal verification of a Hilbert problem. By formalising the DPRM theorem, we see our larger goal as bringing one of the most important mathematical results the twentieth century into the methods of the twenty-first.