A Formal Proof of Complexity Bounds on Diophantine Equations

Jonas Bayer, Marco David

We present a universal construction of Diophantine equations with bounded complexity in Isabelle/HOL. This is a formalization of our own work in number theory. Hilbert's Tenth Prob…