-
Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization
Authors:
Jonas Bayer,
Marco David,
Malte Hassler,
Yuri Matiyasevich,
Dierk Schleicher
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…
▽ More
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 $ν$ and degree $δ$ such that all Diophantine equations can be rewritten in at most this complexity. Our work develops explicit universal pairs $(ν, δ)$ 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.
△ Less
Submitted 29 June, 2025; v1 submitted 25 June, 2025;
originally announced June 2025.
-
A Formal Proof of Complexity Bounds on Diophantine Equations
Authors:
Jonas Bayer,
Marco David
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.
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…
▽ More
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.
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 the main construction required to establish said universal pair. In doing so, we markedly extend the Isabelle AFP entry on multivariate polynomials, formalize parts of a number theory textbook, and develop classical theory on Diophantine equations in Isabelle. 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. We reflect how the close collaboration between mathematician and computer is an uncommon but promising modus operandi.
△ Less
Submitted 22 May, 2025;
originally announced May 2025.
-
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
Authors:
Jonas Bayer,
Aleksey Gonus,
Christoph Benzmüller,
Dana S. Scott
Abstract:
This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic…
▽ More
This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-logical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions.
△ Less
Submitted 16 June, 2023; v1 submitted 15 June, 2023;
originally announced June 2023.
-
Mathematical Proof Between Generations
Authors:
Jonas Bayer,
Christoph Benzmüller,
Kevin Buzzard,
Marco David,
Leslie Lamport,
Yuri Matiyasevich,
Lawrence Paulson,
Dierk Schleicher,
Benedikt Stock,
Efim Zelmanov
Abstract:
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time th…
▽ More
A proof is one of the most important concepts of mathematics. However, there is a striking difference between how a proof is defined in theory and how it is used in practice. This puts the unique status of mathematics as exact science into peril. Now may be the time to reconcile theory and practice, i.e. precision and intuition, through the advent of computer proof assistants. For the most time this has been a topic for experts in specialized communities. However, mathematical proofs have become increasingly sophisticated, stretching the boundaries of what is humanly comprehensible, so that leading mathematicians have asked for formal verification of their proofs. At the same time, major theorems in mathematics have recently been computer-verified by people from outside of these communities, even by beginning students. This article investigates the gap between the different definitions of a proof and possibilities to build bridges. It is written as a polemic or a collage by different members of the communities in mathematics and computer science at different stages of their careers, challenging well-known preconceptions and exploring new perspectives.
△ Less
Submitted 8 July, 2022;
originally announced July 2022.
