Formal reasoning with a computer assistant: A quantitative solution to Hilbert's Tenth Problem

This talk explores the development of mathematical proofs with the assistance of interactive theorem provers. We exemplify this through bounding the complexity of Diophantine equations over the integers, which provides a quantitative negative solution to Hilbert’s Tenth Problem (H10).

 

H10 asks about the decidability of Diophantine equations and has first been answered negatively by Davis, Putnam, Robinson and Matiyasevich in 1970. We ask for which subclasses of equations, defined by bounds on the number of variables and the degree, the problem remains undecidable. Our work develops explicit universal pairs for integer unknowns, achieving bounds that cannot be obtained by naive translations of previously known results.

 

This is one of the first articles in mathematics that has appeared together with a computer-verified certificate of correctness: in parallel to writing a traditional article, we have conducted a formal verification of our results using the proof assistant Isabelle. While formal proof verification has traditionally been applied a posteriori to known results, this project has integrated formalization into the discovery and development process. We will also discuss insights gained from this unusual approach and its implications for mathematical practice.