Pith. sign in

REVIEW 2 major objections 4 minor 5 references

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

T0 review · 2 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Every Diophantine set over the integers can be represented by an equation in 11 unknowns, at the price of a degree given by an explicit closed form.

desk verdict Genuinely new explicit universal pairs over Z with 11 unknowns, backed by a serious Isabelle formalization, but the smaller degree pair in Corollary B rests on Jones's unproved (32,12)_N claim and should be flagged conditional. read the letter →

arxiv 2506.20909 v2 pith:3M5XLK4D submitted 2025-06-26 math.NT cs.LO

Jonas Bayer , Marco David , Malte Hassler , Yuri Matiyasevich , Dierk Schleicher This is my paper · ORCID
classification math.NTcs.LO MSC 11U0503D35
keywords universalpairsDiophantineequationsoverintegersHilbert'stenthproblemdegreeboundsLucassequencesbinomialcoefficientsmachine-checkedproofsets
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper establishes the first explicit universal pairs for Diophantine equations over the integers: from any universal pair $(\nu,\delta)$ over the natural numbers it constructs a universal pair $(11,\eta(\nu,\delta))$ over $\mathbb{Z}$, with $\eta(\nu,\delta) = 15\,616 + 233\,856\,\delta + 233\,952\,\delta(2\delta+1)^{\nu+1} + 467\,712\,\delta^2(2\delta+1)^{\nu+1}$. Plugging in known natural-number universal pairs gives $(11,\approx 1.68105\cdot 10^{63})$ and $(11,\approx 9.50818\cdot 10^{53})$ as universal over $\mathbb{Z}$, meaning every Diophantine subset of $\mathbb{N}$ is represented by an integer polynomial in 11 unknowns of degree bounded by those numbers. If correct, Hilbert's tenth problem has no decision algorithm even for equations with at most 11 unknowns and degree at most about $1.68\cdot 10^{64}$. The proof was developed in parallel with a machine-checked formalization, and the paper reports that the formalization caught wrong numerical values and missing hypotheses.

What carries the argument

The argument is carried by three mechanisms working in sequence. First, a coding-and-masking theorem packs the arguments of an arbitrary polynomial into a single natural number $g$ and converts $P(z)=0$ into a divisibility condition $Y \mid \binom{2X}{X}$, using binary-carry counting and masks. Second, the Bridge Theorem converts the two exponential-looking conditions, $b$ being a power of two and $Y$ dividing the binomial coefficient, into four ordinary Diophantine relations by recognizing Lucas-sequence values through Pell equations; this is where the paper's variable count stays bounded and independent of the original polynomial's degree. Third, a relation-combining polynomial $M_q$ with $q=3$ folds squareness, positivity, and divisibility into one equation, yielding a polynomial $Q$ in a parameter $a$ and nine unknowns, one of which is natural. The final step replaces that natural unknown with three integer unknowns, producing the 11-unknown universal polynomial; Appendix A supplies the degree arithmetic that gives $\eta$.

What would settle it

Check the repository-linked formal proof against the exact statements of Theorem A, Corollary B, and Corollary C, and recompute $\eta$ in Appendix A: if the certified degree differs from $\eta$, or if the formalization does not cover the full construction including the three-squares step and the nine-unknown polynomial, the claimed universal pairs are not established. Independently, finding any Diophantine set over $\mathbb{Z}$ that the constructed 11-unknown polynomial cannot represent would refute the theorem.

Watch

Extended reading notes

Core claim

The central claim is Theorem A: whenever $(\nu,\delta)$ is universal over $\mathbb{N}$, the pair $(11,\eta(\nu,\delta))$ is universal over $\mathbb{Z}$, where $\eta$ is the displayed degree formula. The construction produces, for any polynomial $P$ representing a Diophantine set over $\mathbb{N}$, a polynomial in 11 integer unknowns that has a solution exactly when $P$ has one. Along the way the paper builds an intermediate polynomial $Q$ with nine unknowns, eight integer and one natural, by combining a coding theorem, a bridge theorem that encodes powers of two and binomial-coefficient divisibility through Lucas-sequence and Pell equations, and a relation-combining polynomial that folds several conditions into one equation; the natural unknown is then replaced by three integer unknowns using the three-squares theorem. The degree bound $\eta$ is obtained by a careful polynomial-degree calculation in Appendix A. Corollary B instantiates the theorem with the natural-number universal pairs $(58,4)$ and $(32,12)$, and Corollary C states the consequent undecidability of Hilbert's tenth problem for the class of equations with at most 11 unknowns and degree at most $1.68\cdot 10^{64}$.

Load-bearing premise

The main numerical conclusion rests on the companion machine-checked formalization covering exactly the statements and degree arithmetic of this preprint; the preprint gives a repository link but no version or commit, so the certificate cannot be independently located from the text alone, and the smaller displayed bound additionally depends on a natural-number universal pair cited without proof.

Editorial extensions

If this is right

  • Corollary C holds: Hilbert's tenth problem is unsolvable for the class of Diophantine equations with at most 11 unknowns and degree at most $1.68\cdot 10^{64}$.
  • Any future improvement of a universal pair over $\mathbb{N}$ automatically transfers to a universal pair over $\mathbb{Z}$ with the same 11 unknowns, with degree given by $\eta$.
  • For every Diophantine set $A \subseteq \mathbb{N}$, an explicit integer polynomial in 11 unknowns can be written down whose solvability encodes membership in $A$.
  • The same degree-bound machinery is formalized in a proof assistant, so the large arithmetic in the theorem is certified by machine rather than by hand-checking alone.
  • The $(58,4)$-based universal pair inherits a published proof through the chain, whereas the smaller-degree $(32,12)$-based pair rests on a natural-number pair that the paper says is only mentioned without proof.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the smaller displayed bound $\approx 9.5\cdot 10^{53}$ should be treated as conditional until the $(32,12)_{\mathbb{N}}$ pair receives a proof; the $(58,4)$-based bound $\approx 1.68\cdot 10^{63}$ stands entirely on published ingredients.
  • The construction suggests that the 11-unknown bound over $\mathbb{Z}$ is not an artifact of one coding trick: the intermediate nine-unknown formulation and the three-squares elimination appear robust, so alternative encodings of powers of two might yield equations with more unknowns but far smaller degrees, a trade-off the paper itself proposes exploring.
  • A testable extension would be to rerun the degree calculation with the constant 3 in $b(a,f)$ replaced by other coefficients; the formalization lets one see exactly which later bounds would need to change, and any such tweak that keeps the inequalities valid would immediately improve Corollary B.
  • The paper's parallel formalization workflow suggests that for results whose content is dominated by huge explicit constants, future mathematical practice may reasonably require a machine-checkable certificate as part of the submission.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper develops explicit universal pairs for Diophantine equations over the integers. Theorem A states that any universal pair (ν,δ)_N over the naturals yields a universal pair (11,η(ν,δ))_Z, where η is the explicit polynomial formula η(ν,δ) = 15616 + 233856δ + 233952δ(2δ+1)^(ν+1) + 467712δ^2(2δ+1)^(ν+1). Instantiating with Jones's (58,4)_N gives (11,1.68105·10^63)_Z, and instantiating with Jones's (32,12)_N gives (11,9.50818·10^53)_Z; Corollary C then concludes that Hilbert's tenth problem is unsolvable for equations with at most 11 unknowns and degree at most 1.68·10^64. The proof combines coding techniques (Theorem 1), a bridge theorem through Lucas sequences (Theorem 2), relation combining (Theorem 3), and detailed degree bookkeeping in Appendix A. The paper also reports a parallel Isabelle formalization, with the repository and companion paper [BD25] cited as the certificate of correctness.

Significance. If the central claims hold, this is a substantial contribution: Theorem A provides the first nontrivial universal pairs over Z with 11 unknowns, and it does so without the variable inflation incurred by the naive four-squares or three-squares translations from universal pairs over N. The paper's explicit η formula and its numerical consequences are falsifiable and precisely stated. A notable strength is the claimed machine-checked formalization in Isabelle, together with the authors' candid account of bugs and numerical errors that the formalization caught; this is credible evidence for the reliability of the intricate degree arithmetic. The first universal pair in Corollary B and Theorem A itself are the load-bearing results. However, the second displayed universal pair in Corollary B inherits an unproved premise from Jones, which limits the advertised 'better' bound and needs to be resolved in the revision.

major comments (2)
  1. [§0.3, Corollary B] The second displayed universal pair (11, 9.50818·10^53)_Z is obtained by applying Theorem A to the pair (32,12)_N, which the paper itself states Jones 'does not provide a proof' for in §0.3. Since universality of (32,12)_N is a strong statement about all Diophantine sets, a mention without proof in Jones's paper is not an established theorem. Unless the Isabelle development actually contains a proof of (32,12)_N, this second pair is not a theorem of the paper or of Jones's published work, and the 'better' bound should be removed or explicitly qualified as conditional on an unproved assertion. The first pair, based on Jones's proved (58,4)_N, and Theorem A itself are not affected by this issue.
  2. [§0.2, §7, companion paper [BD25]] The paper claims that the preprint 'appears with a certificate of correctness' and that the formalization covers the main results, but it does not provide a commit hash or any fixed snapshot identifier for the GitLab repository. A reader cannot verify from this text alone that the certificate applies to the exact statements and the exact degree arithmetic of this version of the manuscript, including the numerical values in Corollary B. Please provide a fixed revision identifier and state explicitly which theorems and numerical claims are covered by the machine-checked proof, and whether the formalization proves, assumes, or omits Jones's (32,12)_N claim.
minor comments (4)
  1. [§0.4, Corollary C] Corollary C states the degree bound as 1.68·10^64, while the first universal pair in Corollary B has η(58,4) ≈ 1.68105·10^63. The larger bound is a weaker but still correct statement if the intent is a conservative rounding, but the text should clarify this, since the displayed numbers otherwise appear inconsistent.
  2. [§0.6] The paper correctly credits Sun for Theorems 1, 2, and 3, but the introduction could more clearly separate Sun's original contributions from the new degree bookkeeping and the universal-pair conclusions, especially because the formalization relies on careful restatements of those theorems.
  3. [Appendix A, A.1] The degree calculation for T in Appendix A.1 is terse and depends on the precise reading of Definition 2.1(2.2j); given that the displayed formulas are easy to misparse, a short explanation of the expression for T and its degree would help the reader verify the η formula.
  4. [Section 7] The statement that 'all dependency theorems' were formalized rather than assumed should be reconciled with the explicit note in §0.3 that Jones provides no proof of (32,12)_N; either the formalization proves this pair, or the claim about dependency theorems should be qualified.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the central derivation is a conditional construction from external universal pairs, with degree bookkeeping done in the paper and checked in Isabelle.

full rationale

Theorem A is a genuine implication: it takes an external universal pair (ν, δ) over N and constructs an explicit polynomial in 11 integer unknowns of degree at most η(ν, δ), with η obtained by counting degrees through the paper's own polynomial constructions in Appendices A.1–A.3. Nothing is fitted to data and no prediction is equivalent to an input by construction. The inputs from Sun, Matiyasevich–Robinson, and Jones are external theorems, not self-citations, and the paper gives proofs or precise attributions for the intermediate results it uses. The companion formalization [BD25] and the earlier DPRM formalization [Bay+19] are self-citations, but they are machine-checked certificates and are not the source of the bound; the paper's mathematical argument stands independently. The paper itself flags that Jones mentions (32,12)_N without a proof, which is a real completeness limitation for the second displayed pair in Corollary B, but this is a matter of external support and not circularity. No load-bearing step reduces to its own input, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper is a proof-heavy number theory construction. It fits no parameters to data. It relies on standard classical theorems and on the companion Isabelle formalization for the error-prone degree arithmetic.

assumptions (5)
  • standard math DPRM theorem: every recursively enumerable set of naturals is Diophantine, and Hilbert's tenth problem is undecidable.
    Used as background to define Diophantine sets and universal pairs; cited to Davis, Putnam, Robinson, and Matiyasevich in Section 0.1.
  • standard math Jones's universal pair (58,4)_N over the naturals, and the mentioned pair (32,12)_N.
    Instantiates Theorem A in Corollary B. The (58,4) pair is proved by Jones, while the (32,12) pair is only mentioned there, as the authors explicitly note.
  • standard math Matiyasevich-Robinson relation-combining lemma, Lemma 5.1.
    Used to combine square, divisibility, and positivity conditions into one polynomial; cited from Matiyasevich-Robinson [MR75, Theorem III] and formalized by the authors.
  • standard math Pell equation solution classification via Lucas sequences, Lemma 3.2.
    Used throughout Sections 3 and 4 to translate Lucas sequences into Diophantine conditions; cited to Lehmer and Matiyasevich-Robinson.
  • standard math Gauss-Legendre three-squares theorem, Lemma 6.1.
    Used to replace the natural unknown n by three integer unknowns in Corollary 4; cited to Nathanson [Nat96, Lemma 1.9].

how reviews work

0 comments
Cite this review

Pith. "Pith review of Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization." pith.science (2026). https://pith.science/paper/3M5XLK4D

@misc{pith2026250620909,
  author       = {Pith},
  title        = {Pith review of: Diophantine Equations over $\mathbb Z$: Universal Bounds and Parallel Formalization},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3M5XLK4D}},
  note         = {Machine review of arXiv:2506.20909}
}
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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

5 extracted references · 5 canonical work pages

  1. [9]

    Reduction of an arbitrary dio- phantine equation to one in 13 unknowns

    doi: 10.1007/978-94-010-1138-9_7. REFERENCES 53 [MR75] Yuri Matiyasevich and Julia Robinson. “Reduction of an arbitrary dio- phantine equation to one in 13 unknowns”. In: Acta Arithmetica 27 (1975), pp. 521–553. [MU21] Leonardo de Moura and Sebastian Ullrich. “The Lean 4 Theorem Prover and Programming Language”. In:Automated Deduction — CADE 28. Ed. by An...

    work page arXiv 1975

  2. [251]

    A Lean formalization of Matiyasevi\v{c}'s Theorem

    doi: 10.1007/3-540-58156-1. [Car18] Mario Carneiro. A Lean formalization of Matiyasevich’s Theorem. 2018. doi: 10.48550/ARXIV.1802.01795. 52 REFERENCES [DC23] AnnaDanilkinandLoïcChevalier.“ThreeSquaresTheorem”.In: Archive of Formal Proofs(2023). https://isa-afp.org/entries/Three_Squ ares.html, Formal proof development.issn: 2150-914x. [DPR61] Martin Davis...

    work page Pith review arXiv doi:10.48550/arxiv.1802.01795 2023

  3. [2019]

    On the multiple solutions of the Pell equation

    (Visited on 06/25/2025). [Leh28] Derrick H. Lehmer. “On the multiple solutions of the Pell equation”. In: Annals of Mathematics (2)30 (1928), pp. 66–72. [LF19] Dominique Larchey-Wendling and Yannick Forster. “Hilbert’s Tenth Problem in Coq”. In:4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Ed. by Herman Geuve...

    work page 1928

  4. [2024]

    url: https://www.wolfram.com/mathematica

    work page

  5. [2025]

    The QED Manifesto

    May 2025.doi: 10.48550/arXiv.2505.16963. [Bun94] Alan Bundy. “The QED Manifesto”. In: Automated Deduction - CADE- 12.Vol.814.LectureNotesinComputerScience.Springer,1994,pp.238–

    work page doi:10.48550/arxiv.2505.16963 2025

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.