Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization

TL;DR

This paper establishes new bounds on the complexity of Diophantine equations over integers and demonstrates their formal verification using Isabelle, blending mathematical discovery with formal proof methods.

Contribution

It develops explicit universal bounds for Diophantine equations over integers and integrates formal proof verification into the research process.

Findings

New bounds for Diophantine equations over $\\mathbb Z$

Formal verification of bounds using Isabelle

Insights into the role of formal methods in mathematical discovery

Abstract

This paper explores multiple closely related themes: bounding the complexity of Diophantine equations over the integers and developing mathematical proofs in parallel with formal theorem provers. Hilbert's Tenth Problem (H10) asks about the decidability of Diophantine equations and has been answered negatively by Davis, Putnam, Robinson and Matiyasevich. It is natural to ask for which subclasses of Diophantine equations H10 remains undecidable. Such subclasses can be defined in terms of universal pairs: bounds on the number of variables $\nu$ and degree $\delta$ such that all Diophantine equations can be rewritten in at most this complexity. Our work develops explicit universal pairs $(\nu, \delta)$ for integer unknowns, achieving new bounds that cannot be obtained by naive translations from known results over $\mathbb N$. In parallel, 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 integrates formalization into the discovery and development process. In a final section, we describe key insights gained from this unusual approach and its implications for mathematical practice. Our work contributes both to the study of Diophantine equations and to the broader question of how mathematics is conducted in the 21st century.