Defining the integers in the rationals: the finite parts decided, the theorem not

What changed. On 6 November the repository moved twice: to Version 3, a new manuscript with its collaborators named and a new, far smaller explicit polynomial (a quartic), then to Version 4, a smaller quartic still, each with its own package of checks. Neither quartic is checked here yet.

What still applies. Everything below was decided on the 5 November release. Two parts of it are the same bytes in the current repository: the original large construction and the whole Lean formalization, 86 of 88 files compared one by one, the two differences READMEs. The Lean README now says what the frozen target is: the statement for the original polynomial, not for the Version 4 quartic, which has no Lean statement yet. So the Lean replay, Track B and the bookkeeping of the original construction apply to the original polynomial as the repository holds it today (corpus/zq/version4-tree-check.json).

The claim. Hilbert’s tenth problem asks for an algorithm that decides whether a polynomial equation with integer coefficients has a solution. Over the integers there is none (Matiyasevich, 1970); over the rationals the question is open. Glazer’s manuscript and repository, github.com/elliotglazer/diophantine-z-q, claim the step that would close it: a fixed polynomial whose rational solutions, read in their first coordinate, are exactly the integers. Then no algorithm can decide rational solvability either.

What is in the repository. The polynomial is not written out as a list of terms. It is saved as a recipe of templates that call one another, from which its size can be counted. The proof is a manuscript of arithmetic geometry resting on published theorems. In Lean, a program that checks proofs line by line, 48 helper modules are accepted, and the main statement is there, frozen, with its proof left as sorry: unproved.

What I did. With Claude agents, I wrote down, before any of my code ran on his data, what each check would decide and what would make it fail. Then I decided again, in four lanes and with code of my own, every part of the claim that is finite: the number of variables and the height of the expression; the tower bounds on the degree and the coefficients; his four finite test suites; and his 48 Lean modules, replayed in Lean’s kernel on a rented machine.

What came out. The bookkeeping holds. The polynomial has exactly 292,890,231,905 variables, counted two ways, and its expression height is 256, as stated. The bounds on degree and coefficients follow by exact arithmetic, but only from four named premises; an attempt to remove one of them by computation was refused, because it is not a computation. The statements his suites test hold on 671,659 cases of mine, and his Lean helpers check in the kernel with only the three standard axioms. Then the Lean gap: a proof of his frozen main statement from eight named hypotheses, written with Claude agents in claimbox, checks in the kernel here, and one of his premises, that the point P₀ has infinite order, is now proved outright.

What it means. None of this decides the theorem. It decides what a machine can decide about the claim today and names what it cannot: the deep results the proof rests on, now eight named Lean hypotheses instead of a sorry. The limits come first below, then each lane with its record.

• The theorem is undecided here. The main Lean statement, lean/Frozen/BoundedIntegerPolynomial.lean, is unproved: its proof is sorry, and lane 4 found it elaborates with exactly one such sorry. Nothing on this page decides whether ℤ is Diophantine in ℚ, nor any consequence claimed for it (Mazur’s conjecture, Hilbert’s tenth problem over ℚ).
• The tower bounds rest on four premises. Lane 2 decides the exact arithmetic from them to deg P_* < 2↑↑7 and |c| < 2↑↑8, and nothing more. H1, an explicit bound on primes in arithmetic progressions (Bennett, Martin, O’Bryant and Rechnitzer), as his proof applies it; H2, the inequality M₀ ≤ N_s¹⁰, from his reduction-order and formal-group argument (Silverman); M, the degree and log-norm majorant at each expression height, a lemma of the manuscript, read and not decided; L1, the height 256, certified by lane 1. Without H1 and H2 the arithmetic gives no upper bound at all, so the bounds with no premise are REFUSED.
• H2 is not a computation. It is one inequality about fixed integers, so it is finite in principle, but deciding it directly needs every prime of his catalogue: 22·φ(W) of them, with φ(W) a 432-bit number. His proof of it instead applies three theorems at all of those places at once. Its nine finite ingredients are certified; the theorems are not, so H2 is REFUSED and lane 2 stays conditional on it.
• Lane 3 could replay his cases for one suite of four. His suites come with counts, but their cases are not in his prose: no ranges for the integer compiler’s digit, bit and packed cases (and its “backend” cases are not defined), no evaluation points for the division-polynomial graphs, which his code generates, and only sha256 hashes for the expression suite, with no stated serialization. Recovering them would mean reading his checker code, which a clean-room lane does not do, so those three replays are REFUSED. The statements each suite tests were decided on cases of mine instead; a count of mine that equals his is never presented as a reproduction of his set. The six-contact suite’s reported values were replayed, exactly.
• The Lean helpers check; what they mean is not checked here. The 48 modules check in the kernel, but whether their statements are the ones the manuscript needs is not decided. One second kernel, nanoda, could not finish the full export (a big-integer overflow, a limit of the tool), so the replay rests on leanchecker --fresh; nanoda accepted 47 of the 48 modules one by one.
• The Lean statement now rests on eight hypotheses. Track B decides that his frozen statement follows in Lean from eight named hypotheses (below). None of them is proved here. If any is false, the Lean theorem says nothing. Whether each Lean hypothesis says what the manuscript’s premise says is my reading, not a decision; a screen only checked that none of them contains his statement itself. Their joint consistency is not decided either.
• Some rules came after a first look. Every lane was pre-registered before any of my code ran on his data, and every later rule is dated in the pre-registration: lane 4’s rule for four constructors’ axiom sets was written after a first pass and before the recorded one, its per-module nanoda run during the recorded pass, and its recorder’s census fix after it. One red control of the H2 tool was blind for a structural reason, so a sharper one was added after the run. Lane 2’s red controls came after the pre-registration: a check of the tool, not a pre-registered test. In Track B, the rule for comparing the generator statement with mine (equal up to the names Lean gives its hidden helper proofs) was written after a first pass and before the recorded one.
• One author on both sides. The checks of Track A, the proof of Track B and its decision were all written by me with Claude agents. claimbox proposes and cert-machine decides; the two have one author, so this separates the roles, not the people. No one else has replayed these records yet; an outside replay would be the next step up.

The question. Lane 4 shows that his Lean helpers check and that the main statement is still sorry. Track B asks a narrower question than the theorem: can that frozen statement, his file unchanged, be proved in Lean from named hypotheses, so that what stays open is a list of stated results instead of a sorry?

The proof. claimbox, the claimant of this machine’s Lean proposals, proved it: from eight hypotheses, each a deep result or a premise of the manuscript entering unproved, his frozen statement follows. Claude agents wrote it there; claimbox and this page have one author.

What was decided here. CERTIFIED, as pre-registered. Lean’s kernel accepts the proof three ways, the last replaying every constant it rests on, core and Mathlib included, into an empty environment (34 minutes). My audit finds only the three standard axioms in all 271 of claimbox’s declarations. The statement is his, checked twice: a Lean module of mine states it by taking the type of his frozen theorem from his file, and is proved by claimbox’s theorem; and a syntactic check finds exactly the eight hypotheses followed by his statement. Seven planted wrong variants, a changed conclusion, an extra hypothesis, a circular one, a sorry, a new axiom, a proof that skipped the kernel and a changed byte, were each caught. Every second, independent checker stopped on a resource limit before reaching a verdict (nanoda on a big-integer overflow, as in lane 4; con-ron and con-leche as Lean ships them on their computation budget; both of their master branches on a stack overflow, also on a 128 GB machine), so the kernel replay rests on Lean’s own checker, as lane 4’s does. On the planted variants nanoda did reach a verdict, and refused each for its planted reason.

One premise is now proved. That his point P₀ = ((1641 − 1160s)/8, (−123720 + 87483s)/32) has infinite order on y² = x³ − d²x with d = 75 − 53s, over ℚ(s) with s² = 2: the first half of his generator proposition. claimbox proves it at the prime 2, the way the manuscript argues elsewhere; the kernel accepts it, CERTIFIED, and the point and the curve in the Lean statement are the manuscript’s, number for number (CERTIFIED).

The eight hypotheses, in the order the theorem takes them, each in my reading, with where the manuscript has it:

• M. a polynomial of bounded size whose rational zeros are exactly the code triples of multiplication, (ι(a), ι(b), ι(ab)) (premise M, the multiplication section).
• H. the height bound h(u) ≤ H₆·M(u)²⁴ for every rational u outside the six contact points (the height theorem (thm:height)).
• PC. every rational B of the stated local shape is a value at which his pole polynomial has a rational zero (the pole hypothesis (hyp:PC)).
• C. a polynomial of bounded size that defines the precision machine’s closeness relation exactly (premise C, the compiler section).
• LT. a polynomial of bounded size carrying the six local tests, sound and complete (lem:test and lem:test-complete).
• CC. for every n outside the contact points and every κ ≠ 0, the precision machine accepts some run (eq:close-complete).
• H1. the explicit bound on primes in arithmetic progressions, as the cutoff proof applies it (proof of prop:cutoff (Bennett–Martin–O’Bryant–Rechnitzer)).
• H2. a formal multiple of P₀ of index at most N_s¹⁰ with the required divisibility, the same H2 as lane 2’s (proof of prop:cutoff (Silverman)).

What it does not mean. It does not prove that ℤ is Diophantine in ℚ: the theorem now rests on these eight, as lane 2’s bounds rest on theirs. If any of them is false, the Lean theorem says nothing. The readings above are mine, not decisions; the record keeps each hypothesis as Lean prints it. The plan this answers is this repository’s gap map, corpus/zq/gap-map.json, which named seven of them; building the proof found two more inputs (LT and CC) and proved one (G).

• Get his repository at the pin. git clone https://github.com/elliotglazer/diophantine-z-q, then git -C diophantine-z-q checkout 97cec7fdd757d9a8e4f468151a47a6d3610fb2f2. Point ZQ_REPO at the clone (the default is ~/Projects/zq-scout/diophantine-z-q).
• Re-derive the records. In a clone of cert-machine, run node tools/zq-recount.js --check, node tools/zq-tower.js --check, node tools/zq-h2.js --check, node tools/zq-finite.js --check, node tools/record-zq-lean-replay.js --check. Each checks the sha256 of every file of his it reads against the pin before reading it, derives its record again and refuses on any difference. They need Node and its standard library, and his clone at the pinned commit.
• The Lean replay. It ran on a rented machine with tools/runpod-zq-lane4.sh; the facts of the run are in corpus/zq/runs/lane4-2026-11-06/. The recorder’s --check derives again from your clone what can be derived on a laptop (the census, the re-hash, the reconciliation with his 704 declarations) and refuses if a script that ran on that machine has changed since.
• The Lean gap. claimbox’s proof is public on its branch zinq-2026-11-06. It was decided on a rented machine with tools/runpod-zq-trackb.sh, the facts in corpus/zq/runs/trackb-2026-11-06/; node tools/record-zq-trackb.js --check derives the record again from those facts and the manuscript’s numbers, and refuses if a script that ran there has changed since. Its pre-registration: notes/zq-trackb-preregistration-2026-11-06.md.
• Nothing of his is copied here. His repository has no licence (its README: licences for original project material are awaiting the maintainer’s selection), so no file of it is in this repository or on this site. Every tool reads his files from your clone; the page quotes his statement only.
• Read the pre-registration. notes/zq-preregistration-2026-11-06.md: what each lane would decide and what would make it fail, written before any code ran on his data, with its dated amendments.