Email Gateway (Jul 29 2025 at 18:36): Email Gateway (Jul 29 2025 at 18:36):From: Tobias Nipkow <nipkow@in.tum.de>
Universal Pairs for Diophantine Equations
Marco David, Théo André, Mathis Bouverot-Dupuis, Eva Brenner, Loïc Chevalier,
Anna Danilkin, Charlotte Dorneich, Kevin Lee , Xavier Pigé, Timothé Ringeard,
Quentin Vermande, Paul Wang, Annie Yao, Zhengkun Ye and Jonas Bayer
We formalize a universal construction of Diophantine equations with bounded
complexity. This is a formalization of our own work in number theory.
Hilbert's Tenth Problem was answered negatively by Yuri Matiyasevich, who showed
that there is no general algorithm to decide whether an arbitrary Diophantine
equation has a solution. However, the problem remains open when generalized to
the field of rational numbers, or contrarily, when restricted to Diophantine
equations with bounded complexity, characterized by the number of variables
v and the degree d. If every Diophantine set can be represented within the
bounds (v,d), we say that this pair is universal, and it follows that the
corresponding class of equations is undecidable. In a separate mathematics
article, we have determined the first non-trivial universal pair for the case of
integer unknowns.
This AFP entry contributes the main construction required to establish said
universal pair. In doing so, we markedly extend previous work on multivariate
polynomials, and develop classical theory on Diophantine equations.
Additionally, our work includes metaprogramming infrastructure designed to
efficiently handle complex definitions of multivariate polynomials. Our
mathematical draft has been formalized while the mathematical research was
ongoing, and benefitted largely from the help of the theorem prover.
https://www.isa-afp.org/entries/Diophantine_Universal_Pairs.html
Wow! At the very least I think it wins the prize for the largest number of
authors of any AFP entry ;-)
Tobias
Last updated: Aug 20 2025 at 20:23 UTC