Document Open Access Logo

A Formal Proof of Complexity Bounds on Diophantine Equations

Authors Jonas Bayer , Marco David

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.3.pdf
  • Filesize: 0.87 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.3.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Diophantine Equations
  • Hilbert’s Tenth Problem
  • Isabelle/HOL

Metrics

Abstract

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 [Jonas Bayer et al., 2025].
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 ν and the degree δ. If every Diophantine set can be represented within the bounds (ν, δ), 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. 
In this paper, we contribute a formal verification of this new result. In doing so, we markedly extend the Isabelle AFP entry on multivariate polynomials [Christian Sternagel et al., 2010], formalize parts of a number theory textbook [Melvyn B. Nathanson, 1996], and develop classical theory on Diophantine equations [Yuri Matiyasevich and Julia Robinson, 1975] in Isabelle. In addition, 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 benefited largely from the help of the theorem prover. We reflect on how the close collaboration between mathematician and computer is an uncommon but promising modus operandi.

Cite As Get BibTex

Jonas Bayer and Marco David. A Formal Proof of Complexity Bounds on Diophantine Equations. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.3

Author Details

Jonas Bayer
  • Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, UK
Marco David
  • Department of Physics, University of California, Berkeley, CA, USA

Acknowledgements

This project would not exist without Yuri Matiyasevich who proposed the formalization of Hilbert’s Tenth Problem and encouraged our exploration of Universal Pairs. We are deeply grateful to Dierk Schleicher for his unwavering support throughout, both on a personal level and through his mathematical insight. We thank Malte Haßler, Thomas Serafini and Simon Dubischar for their mathematical contributions to the project. We are indebted to the group of students who contributed at various stages of the formalization. In particular, we thank Timothé Ringeard and Xavier Pigé for leading the formal proof of the Bridge Theorem; Anna Danilkin and Annie Yao for their work on poly_extract, poly_degree and further developments in multivariate polynomial theory; Mathis Bouverot-Dupuis, Paul Wang, Quentin Vermande, and Theo André for their formalization of coding theory; Loïc Chevalier, Charlotte Dorneich, and Eva Brenner for the formalization of Matiyasevich’s polynomial and relation combining; and Zhengkun Ye and Kevin Lee for their contributions to formal degree calculations. The above highlights their primary contributions, though many have supported other aspects of this work whenever they were able. We also thank all other members of the student work group for their involvement in the project. We gratefully acknowledge support from the Département de mathémathiques et applications at École Normale Supérieure de Paris.

Supplementary Materials

References

  1. Jonas Bayer, 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, and Zhengkun Ye. Universal Pairs for Diophantine Equations . Software (visited on 2025-09-09). URL: https://www.isa-afp.org/entries/Diophantine_Universal_Pairs.html
    full metadata available at: https://doi.org/10.4230/artifacts.24709
  2. Jonas Bayer, Marco David, Malte Haßler, Yuri Matiyavsevich, and Dierk Schleicher. Diophantine Equations over ℤ: Universal Bounds and Parallel Formalization, 2025. URL: https://arxiv.org/abs/2506.20909.
  3. Jonas Bayer, Marco David, Abhik Pal, and Benedikt Stock. Digit expansions. Archive of Formal Proofs, April 2022. Formal proof development. URL: https://isa-afp.org/entries/Digit_Expansions.html.
  4. Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM Theorem in Isabelle. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1-33:7, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.33.
  5. Mario Carneiro. A Lean formalization of Matiyasevič’s Theorem, 2018. arxiv: https://arxiv.org/abs/1802.01795. URL: https://doi.org/10.48550/arXiv.1802.01795.
  6. Anton Danilkin and Loïc Chevalier. Three Squares Theorem. Archive of Formal Proofs, 2023. Formal proof development. URL: https://isa-afp.org/entries/Three_Squares.html.
  7. David Hilbert. Mathematische Probleme. Archiv der Mathematik und Physik, 1:44-63, 213-247, 1901. Google Scholar
  8. James P. Jones. Universal Diophantine equation. The Journal of Symbolic Logic, 47(3):549-571, 1982. URL: https://doi.org/10.2307/2273588.
  9. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:20, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.27.
  10. Yuri Matiyasevich. The Diophantineness of enumerable sets. Dokl. Akad. Nauk SSSR, 191:279-282, 1970. Google Scholar
  11. Yuri Matiyasevich. Some Purely Mathematical Results Inspired by Mathematical Logic, pages 121-127. Springer Netherlands, Dordrecht, 1977. URL: https://doi.org/10.1007/978-94-010-1138-9_7.
  12. Yuri Matiyasevich. Hilbert’s Tenth Problem. Foundations of Computing Series. MIT Press, 1993. Google Scholar
  13. Yuri Matiyasevich. The Riemann Hypothesis in computer science. Theoretical Computer Science, 807:257-265, 2020. In memory of Maurice Nivat, a founding father of Theoretical Computer Science - Part II. URL: https://doi.org/10.1016/j.tcs.2019.07.028.
  14. Yuri Matiyasevich and Julia Robinson. Reduction of an arbitrary Diophantine equation to one in 13 unknowns. Acta Arithmetica, 27:521-553, 1975. Google Scholar
  15. Melvyn B. Nathanson. Additive number theory. The classical bases, volume 164 of Graduate texts in mathematics. Springer, New York, 1996. Google Scholar
  16. Karol Pak. Formalization of the MRDP Theorem in the Mizar system. Formalized Mathematics, 27(2):209-221, 2019. URL: https://doi.org/10.2478/forma-2019-0020.
  17. Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler, and Alexander Bentkamp. Executable multivariate polynomials. Archive of Formal Proofs, 2010. Formal proof development. URL: https://isa-afp.org/entries/Polynomials.html.
  18. Zhi-Wei Sun. Reduction of unknowns in Diophantine representations. Science in China Series A, 35(3):257-269, 1992. Google Scholar
  19. Zhi-Wei Sun. Further results on Hilbert’s Tenth Problem. Science China Math, 64(2):281-306, 2021. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact