{"id":"7f037462-35c3-4c25-84d0-f39061241b98","arxiv_id":"2506.20909","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"low","formal_verification":"full","parameter_count":0,"one_line_summary":"Every Diophantine set over the naturals has an integer representation with only 11 unknowns and degree below an explicit but huge bound.","lead":"This paper constructs explicit universal pairs over the integers: every Diophantine set over the naturals can be represented by a polynomial with 11 integer unknowns, at the price of an enormous degree. The proof was developed together with a machine-checked Isabelle formalization, which the authors say caught wrong numerical values in an earlier version of the project.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Corollary B's second universal pair rests on Jones's (32,12)_N claim, which the paper itself says Jones does not prove; as stated, that pair is not established.","rationale":"Good faith: the paper is unusually transparent, the main construction is formalized, and a spot-check of the Appendix A degree arithmetic is consistent with the claimed η up to the factor of 8 in the final multiplication. The reason for CONDITIONAL rather than ACCEPT is not primarily the absence of a commit hash; it is that one of the two numerical conclusions in Corollary B has an unproved premise. The authors themselves flag this in prose, but the theorem statement does not. If the Isabelle formalization contains a proof of (32,12)_N, this concern is resolved; if it treats it as an axiom, the certificate should state the assumption. This concern is narrow and does not affect Theorem A or the first pair in Corollary B.","tokens_in":43426,"tokens_out":28002,"duration_ms":257199,"concrete_test":"Check Jones (1982), \"Universal Diophantine equation\", for a theorem or lemma establishing (32,12)_N as a universal pair, and inspect the companion Isabelle development (GitLab / [BD25]) for whether \"(32,12)_N is universal\" appears as a proved theorem or as an axiom/assumption. If no proof exists, split Corollary B: keep the (58,4)-derived pair as proven and explicitly mark the (32,12)-derived pair conditional.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central implication Theorem A is conditional: it turns any universal pair (ν,δ)_N into (11,η(ν,δ))_Z. Applying it to (32,12)_N therefore inherits the full burden of proving that (32,12)_N is universal over N. In §0.3, immediately before Corollary B, the authors state that Jones \"does not provide a proof\" for (32,12)_N. If that is accurate, the second displayed universal pair in Corollary B, (11, 9.50818·10^53)_Z, is not a theorem of the paper or of Jones's published work. The formalization does not repair this unless the Isabelle development contains a proof of (32,12)_N; if it instead assumes it as an axiom, the certificate proves a conditional statement. The first pair, obtained from Jones's proved (58,4)_N, is unaffected, as is Theorem A itself. The issue is local but load-bearing for the paper's advertised \"better\" bound and for Corollary C's smaller degree.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":43578,"tokens_out":12967,"duration_ms":127875,"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":[{"comment":"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.","section":"§0.3, Corollary B"},{"comment":"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.","section":"§0.2, §7, companion paper [BD25]"}],"minor_comments":[{"comment":"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.","section":"§0.4, Corollary C"},{"comment":"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.","section":"§0.6"},{"comment":"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.","section":"Appendix A, A.1"},{"comment":"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.","section":"Section 7"}],"recommendation":"major_revision","confidential_remarks":"The central mathematical construction and Theorem A appear sound, and the first universal pair in Corollary B is well supported. The main obstacle is the second pair in Corollary B, which rests on an unproved assertion attributed to Jones. If the authors can confirm that the Isabelle development contains a proof of (32,12)_N, or if they relegate the second pair to a clearly conditional statement, the paper would be close to acceptance. I did not independently re-run the certificate, so pinning the repository to a specific commit is important for the reproducibility claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe paper you'd want to know about: it gives the first explicit universal pairs over Z with 11 unknowns, with degrees around 10^63. The main engine is Theorem A: if (ν,δ) is universal over N, then (11, η(ν,δ)) is universal over Z, with η spelled out as a closed form. That is a real, new result, and the proof is a careful composition of Sun's coding theorems, Matiyasevich–Robinson relation combining, and Jones's universal pairs over N. Credit is given where due, especially to Sun.\n\nThe strongest evidence is the Isabelle formalization. The authors say the whole development is machine-checked and point to a repository and a companion ITP paper. That is real evidence, and it shows in the text: the degree calculations are explicit, and the identification of several bugs in earlier drafts is candid. I take the central theorem as likely sound.\n\nNow the soft spots. First, the smaller universal pair in Corollary B, (11, 9.5×10^53), is obtained by applying Theorem A to Jones's (32,12)_N pair, which the authors themselves say Jones does not prove. As stated, Corollary B presents both pairs as theorems, but the second one is only as good as an unproved assertion from the literature. If the Isabelle development proves (32,12)_N, say so; if it assumes it as an axiom, the certificate proves a conditional. This is local, but it is load-bearing for the paper's advertised 'better' bound and for Corollary C's smaller degree. The first pair, from Jones's (58,4)_N, is unaffected.\n\nSecond, the manuscript gives no commit hash or build instructions for the formalization. A reader cannot re-check the certificate from this text alone. That is a minor omission for an arXiv preprint, but for a paper whose central claim is 'formally verified,' a stable reference should be part of the record.\n\nThe self-reported history of wrong numbers in an earlier publication is a caution, but not a reason to doubt the present version; the formalization is the corrective. All told, the central argument holds up as far as I can see, and the conditional second pair is the one thing a referee should push on.\n\nThis paper deserves a serious referee. I would send it to review, with the requirement that the authors either prove or clearly mark the (32,12)_N dependency, and pin down the formalization artifacts. I would cite the first pair, not the second.\n\nBest,","headline":"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.","tokens_in":44142,"tokens_out":2789,"would_cite":true,"duration_ms":30999,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["11U05","03D35"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["universal pairs","Diophantine equations over integers","Hilbert's tenth problem","degree bounds","Lucas sequences","binomial coefficients","machine-checked proof","Diophantine sets"],"falsifier":"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.","tokens_in":43204,"feed_emoji":"🔢","tokens_out":9635,"duration_ms":97252,"temperature":0.7,"pith_summary":"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.","feed_headline":"Eleven unknowns keep Hilbert's tenth problem undecidable","feed_subtitle":"New universal pairs over Z bound degree by ≈10^63, and no algorithm can decide solvability in this class.","key_machinery":"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$.","core_discovery":"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}$.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the known universal pairs $(58,4)_{\\mathbb{N}}$ and $(32,12)_{\\mathbb{N}}$ over natural numbers that the paper substitutes into $\\eta$.","marker":"[Jon82]"},{"why":"Gives the relation-combining polynomial $M_q$ and the earlier 13-unknown reduction technique that the construction extends.","marker":"[MR75]"},{"why":"Provides Theorems 1 through 3, the coding, bridge, and nine-unknown formulations that the paper adapts to derive universal pairs over $\\mathbb{Z}$.","marker":"[Sun21]"},{"why":"Classical source for the description of Lucas sequences as solutions of Pell equations, used in Lemma 3.2.","marker":"[Leh28]"},{"why":"Supplies the three-squares theorem used in Lemma 6.1 to replace the one natural unknown with three integer unknowns.","marker":"[Nat96]"},{"why":"Companion formal proof paper that provides the machine-checked certificate for the numerical claims in this preprint.","marker":"[BD25]"}],"fun_headline_variants":["Eleven unknowns, degree ~10^64: H10 remains undecidable","Hilbert's tenth: 11 variables suffice over the integers","Tighter Diophantine bounds: 11 unknowns, degree ~10^64","Formal Isabelle proof accompanies new Diophantine bounds"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Eleven unknowns, degree ~10^64: H10 remains undecidable","Hilbert's tenth: 11 variables suffice over the integers","Tighter Diophantine bounds: 11 unknowns, degree ~10^64","Formal Isabelle proof accompanies new Diophantine bounds"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00076,"raw_usage":{"total_tokens":3419,"prompt_tokens":1035,"completion_tokens":2384,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":651,"completion_tokens_details":{"reasoning_tokens":2306}},"tokens_in":651,"tokens_out":2384,"duration_ms":18829,"temperature":1.0,"reasoning_tokens":2306,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T22:39:59.449174+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}