2 Search Results for "Schleicher, Dierk"

Document
DOI: 10.4230/LIPIcs.ITP.2025.3
A Formal Proof of Complexity Bounds on Diophantine Equations

Authors: Jonas Bayer and Marco David

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

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

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)

Copy BibTex To Clipboard

@InProceedings{bayer_et_al:LIPIcs.ITP.2025.3,
  author =	{Bayer, Jonas and David, Marco},
  title =	{{A Formal Proof of Complexity Bounds on Diophantine Equations}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{3:1--3:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.3},
  URN =		{urn:nbn:de:0030-drops-246023},
  doi =		{10.4230/LIPIcs.ITP.2025.3},
  annote =	{Keywords: Diophantine Equations, Hilbert’s Tenth Problem, Isabelle/HOL}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2019.33
The DPRM Theorem in Isabelle (Short Paper)

Authors: Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
Hilbert’s 10th problem asks for an algorithm to tell whether or not a given diophantine equation has a solution over the integers. The non-existence of such an algorithm was shown in 1970 by Yuri Matiyasevich. The key step is known as the DPRM theorem: every recursively enumerable set of natural numbers is Diophantine. We present the formalization of Matiyasevich’s proof of the DPRM theorem in Isabelle. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. Using several number-theoretic lemmas, we prove that exponentiation has a diophantine representation. Further, we contribute a small library of number-theoretic implementations of binary digit-wise relations. Finally, we discuss and contribute an is_diophantine predicate. We expect the complete formalization of the DPRM theorem in the near future; at present it is complete except for a minor gap in the arithmetization proofs of register machines and extending the is_diophantine predicate by two binary digit-wise relations.
Cite as

Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM Theorem in Isabelle (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 33:1-33:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bayer_et_al:LIPIcs.ITP.2019.33,
  author =	{Bayer, Jonas and David, Marco and Pal, Abhik and Stock, Benedikt and Schleicher, Dierk},
  title =	{{The DPRM Theorem in Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{33:1--33:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.33},
  URN =		{urn:nbn:de:0030-drops-110883},
  doi =		{10.4230/LIPIcs.ITP.2019.33},
  annote =	{Keywords: DPRM theorem, Hilbert’s tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2019

  • Refine by Author
  • 2 Bayer, Jonas
  • 2 David, Marco
  • 1 Pal, Abhik
  • 1 Schleicher, Dierk
  • 1 Stock, Benedikt

  • Refine by Series/Journal
  • 2 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Higher order logic
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 DPRM theorem
  • 1 Diophantine Equations
  • 1 Diophantine predicates
  • 1 Formal verification
  • 1 Hilbert’s Tenth Problem
  • Show More...

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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact