PIRSA:25100157

Video URL

https://pirsa.org/25100157

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

David, M. (2025). Formal reasoning with a computer assistant: A quantitative solution to Hilbert's Tenth Problem. Perimeter Institute for Theoretical Physics. https://pirsa.org/25100157

David, Marco. Formal reasoning with a computer assistant: A quantitative solution to Hilbert's Tenth Problem. Perimeter Institute for Theoretical Physics, Oct. 14, 2025, https://pirsa.org/25100157 

          @misc{ scivideos_PIRSA:25100157,
            doi = {10.48660/25100157},
            url = {https://pirsa.org/25100157},
            author = {David, Marco},
            keywords = {Quantum Foundations},
            language = {en},
            title = {Formal reasoning with a computer assistant: A quantitative solution to Hilbert{\textquoteright}s Tenth Problem},
            publisher = {Perimeter Institute for Theoretical Physics},
            year = {2025},
            month = {oct},
            note = {PIRSA:25100157 see, \url{https://scivideos.org/pirsa/25100157}}
          }

Marco David University of California, Berkeley

Talk numberPIRSA:25100157
DOI10.48660/25100157
Source RepositoryPIRSA
Collection
Talk Type Scientific Series
Subject

Abstract

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.