#952, the Gaussian moat: no walk to infinity through the Gaussian primes in steps of bounded length — OpenAI's proof, its Lean replayed here and its paper read by AI seats; Formal Conjectures' statement, marked solved but still sorry, proved in Lean from it

The problem. Erdős problem #952 [Er77c; Er80, p. 114]: "Is there an infinite sequence of distinct Gaussian primes x₁, x₂, … such that |x_n+1 − x_n| ≪ 1?" The page itself says this is not really a problem of Erdős: Erdős recalled that Motzkin told it to him in November 1963 and that it was apparently raised by Basil Gordon and Motzkin, and in [Er80] he wrote that "the answer is almost certainly negative". It is the Gaussian moat problem. When we read the page on 22 October 2026 it had no proof claims, its comment box was suspended, it had last been edited on 8 April 2026, and it did not mention OpenAI's release; the community database (teorth/erdosproblems) still lists #952 as open.

The claim. OpenAI, "Bounded-Step Walks on Gaussian Primes" (dated 26 September 2026, 29 pages, released 6 October as family 28 of github.com/openai/math). Theorem 1.1: for every finite real D there is a finite B_D such that every connected component of G_D has at most B_D vertices. G_D joins two Gaussian primes when they are at distance at most D, and the primes on the axes count. So every walk through distinct Gaussian primes with steps of length at most D has at most B_D points, and the answer to #952 is no. This uniform form is the conjecture of Gethner and Stark (1997, p. 290), and Vardi stated it as his Conjecture 1.2 (1998). The bound is not explicit. The paper reduces Theorem 1.1 (§2, Proposition 2.1) to Theorem 1.2, a finite sieve. For every D ≥ 1 there is a finite set P_D of rational primes p ≡ 1 (mod 4) such that the set A(P_D) of Gaussian integers divisible by neither factor π_p, π̄_p of any p in P_D contains no infinite walk with steps ≤ D. Every Gaussian prime that is not an associate of one of the finitely many removed factors lies in A(P_D). A(P_D) is periodic modulo Q = ∏p. In a periodic set with no infinite walk, every component is finite (the graph is locally finite, so an infinite component would contain an infinite walk), and no component has more than Q² points, since two points of one component that differ by a period would make it invariant under that translation, which a finite set cannot be. Adding back the removed factors costs a bounded amount. The paper's bound is max{Q², |E| + (K_D − 1)|E|Q²}, where E is the set of associates of the removed factors and K_D counts the lattice points within distance D of 0. The Lean proves its own bound by the same route; this formula is checked by reading only.

The argument. Fix any infinite self-avoiding walk with steps ≤ D, deterministic and arbitrary. Sample times along it and look at the joint distribution of the walk's residues modulo many split Gaussian primes. §4: a stretch of n steps spans a region of area A ≥ cn and has at least c_DA distinct differences (Lemma 4.1, a degree argument on a torus), and a product of randomly chosen factors π or π̄ over many primes in [T, 2T] almost never divides a nonzero vector in a thin rectangle (Lemma 4.2, via the isoperimetric inequality on the Boolean cube). So choosing an endpoint of a uniformly random difference pushes the residue entropy toward its maximum (Lemma 4.3). §5: a coverage-transfer theorem (5.2) turns near-maximal joint entropy, together with coverage at a later checkpoint, into coverage at an earlier one: the terminal residue modulo most factors of norm p gives every residue mass at least τ/p, outside fewer than p^1−β exceptions. §6 arranges all this in one schedule of sampling scales, at prime batches T with log T ≈ 100^m, ending at one common random time t_*. §7: if the walk avoids zero modulo every selected factor, a short word of L ≈ T^2/5 increments, too short to revisit a residue modulo a prime of norm ≥ T, must reveal at least c₁/log T nats of information per increment about the residues (Proposition 7.1). §8: those charges telescope, so their sum over all batches is at most log K_D + o(1), and log K_D bounds the entropy of one increment (Lemma 8.1). But Σ 1/log T over the batches grows like the number of windows, so for one large enough M, depending only on D, no such walk can exist. The paper calls the method "related to Tao's entropy-decrement argument". Our gloss, not the paper's, of the heuristic behind it: keeping a walk inside a set of density ρ costs log(1/ρ) per step, here Σ 2/p ≈ Σ 1/log T, and one step has at most log K_D to spend.

The Lean, and our replay. OpenAI's Lean is 41 modules (12,703 lines) under OAI/NumberTheory/GaussianMoat/, importing only Mathlib. Its theorem OAI.GaussianMoat.fullMain : MainEndpoint ∧ UniformEndpoint states, first, that no injective sequence of irreducible Gaussian integers has dist (z (t+1) : ℂ) (z t : ℂ) ≤ D for all t, for any real D. Second, for every real D there is B bounding the size of every component of the bounded-step prime graph, which is also proved finite, and the length of every injective finite walk. We compiled the closure at openai/math commit 1581d4c (Lean 4.34.1, Mathlib d13f23b), lake-free and in dependency order, on 22 October. We were not the first. plasma-ai's erdos wiki (7 October), carlostoledo1891/cert-machine (10 October, with Lean's kernel and the independent nanoda kernel) and RichardGeorgeDavis's research-artifact-ledger (12 October) report builds of the same theorem. Ours is an independent replication with the controls below. The result: 41 of 41 modules, 0 errors, 7 min 39 s with four workers, peak 6.7 GiB per process. #print axioms under --trust=0 gives exactly propext, Classical.choice, Quot.sound. The theorem and its five definitions (PrimeVertex, primeGraph, component, MainEndpoint, UniformEndpoint) print identically under pp.all in ComparatorChallenges/GaussianMoat.lean, the statement the release's scope note designates for comparison, which is the theorem with sorry. Our matcher fails on each of seven deliberate corruptions of its inputs (three token changes, a smuggled axiom, a comparator without sorry, a missing block, a missing log), and a planted sorry shows up as sorryAx. No file in the 41 contains sorry, axiom, native_decide, implemented_by or unsafe. The coercion is Mathlib's GaussianInt.toComplex and the distance is Mathlib's metric on ℂ, so the statement is the Euclidean one. Formal Conjectures cites commit adc7f12, OpenAI's initial commit of 6 October. The GaussianMoat directory has the same git tree (c84262a9) at adc7f12, at fd4aeeb and at 1581d4c. The comparator files, the scope note and the preprint are also unchanged across those commits. We also ran leanchecker --fresh, which re-checks every declaration from scratch, Mathlib's included, over the 41 modules together with our bridge (below). It exited 0 after 3,480 s with a peak of 8.2 GiB. The same command on a module that does not exist exits 1.

The Lean is not a transcript of the paper. A seat that read the comparator, Model.lean, Main.lean and the declarations that carry the argument across the 41 files, against the printed paper, found that the formal proof takes a different route in four places. (1) It does not use the prime number theorem in progressions (3.1): it gets a positive proportion of dense dyadic batches of primes ≡ 1 (mod 4) from Mathlib's Dirichlet L-function results. (2) It replaces the torus-degree proof of Lemma 4.1 with a discrete Sperner-type argument. (3) It does not formalise §6.3–6.4 as printed, that is, the ladder of checkpoints A₀, …, A_J with β_i = 2⁻ⁱβ₀ and the backward induction of Proposition 6.2. Instead it proves the terminal coverage that §7 consumes from a base case with a constant fraction of exceptions and one transfer step. (4) It fixes the number of windows from D and lets the base scale grow, where the paper lets the number of windows grow. Theorem 1.1 is machine-checked all the same. Five parts of the printed paper rest on reading alone, by our seats and by us: the use of (3.1), the torus-degree proof of Lemma 4.1, the growing-window schedule of §6.1 with Lemma 6.1, the ladder of §6.3–6.4 with Proposition 6.2, and the explicit bound in Proposition 2.1. A hole found there would be a hole in the exposition, not in the theorem. Neither the paper nor the release's scope note (lean/docs/028.md) says that the formal proof takes another route.

The reading. Five Opus 5.5 seats read the paper and its Lean. Each was briefed to refute one part, to quote the sentence it objected to by the paper's printed numbering, and to run small checks wherever a statement allowed one. G took §§1–4, S took §§5–6, I took §§7–8, L read the Lean against the paper and the statement, and W took the sources, priority and the public record. All five returned HOLDS AS READ. None found a gap or an error; they made only exposition notes. Their checks include: Lemma 4.1 on 1,547 walks; the cube inequality (4.2) over all 65,535 nonempty vertex sets of the 4-cube; an exact experiment on Lemma 4.2's tail bound; Lemma 5.1 computed exactly on ten split primes, with a control that drops its shared-cost term and fails; a Monte Carlo of Theorem 5.2's list bound at p = 4,001, with a dependent-trials control that fails; the recursions for τ_i, η_i and r_i in exact rationals for i < 1,500; and every explicit inequality of §§5–6 at every checkpoint, for seven batch sizes in each window, for M = 84, 86 and 90, with generous stand-ins for the constants the paper leaves unnamed. The same check still passes with much heavier stand-ins (C_D = 10⁹, g₀ = 10⁻⁶, at M = 90 and 120). It fails, each time at the inequality that should break, when any one of four of the paper's choices is weakened: the exponent 6/5 in n_i, the gap 2β_i between checkpoints, g₁ = e^−M³ and g₂ = e^−100M²⁰. I's verdict on §§7–8 depended on five statements imported from §6. S checked each in the exact form §§7–8 use it. S also wrote out the order in which the constants are fixed: D; then e₀, a₀, l₀ and the prime-count constant; then g₀, c₀, B and finally M. No threshold depends on the walk, the batch or the starting time. S's exposition notes: (1) the paper's own list of that order omits a₀ and the prime-count constant; (2) Lemma 4.3 is stated for an asymptotic family but used at many (U, g, T) at once, which needs its error constant to be independent of g, and it is; (3) the bound (6.8) goes through Lemma 6.1 without saying so; (4) the display (6.17) is never used. A helper script left by an earlier seat had reported failures in §6. They were 30-digit rounding artefacts, and S replaced the script before relying on anything it said. Seat L's notes concern the Lean: the comparator's definition list is empty, so the five definitions are protected only by the dependency check and by our pp.all match. W's notes are in the next paragraph. The seats coordinating this entry also read all eight sections themselves and found nothing. Nobody checked the absolute constants of Lemma 4.2 or the O(·) bookkeeping of Lemma 4.3 to the last digit; the Lean checks those.

Formal Conjectures, and the bridge (ours). Formal Conjectures' Erdos952.erdos_952 (FormalConjectures/ErdosProblems/952.lean) has been tagged "research solved" since 11 October (PR #6898), citing OpenAI's Lean, but its proof is sorry. The PR's own description, under the heading "Reviewer notes", lists "Erdős 952 (norm vs distance)" among links whose theorem differs from FC's statement "by a routine transport that is not in the linked proof". It now states (since 14 October) ¬ ∃ (x : ℕ → GaussianInt) (C : ℤ), Function.Injective x ∧ ∀ n, Prime (x n) ∧ (x (n + 1) - x n).norm < C, with steps measured by the integer norm and primality as Prime. We copied that statement into our own file (FC at commit 3b7c94ec, 21 October). A script checks the copy word for word after whitespace normalisation and fails on a one-token mutation. We proved it from the first conjunct of OpenAI's fullMain with D = √C, using a lemma dist (a : ℂ) (b : ℂ) = √(a − b).norm. We also proved a uniform form from the second conjunct: for every C : ℤ there is B : ℕ bounding the length of every injective finite sequence of primes whose consecutive differences have norm < C. Both are on the three standard axioms. The controls: the same file with the proof that invokes OpenAI's theorem replaced by sorry reports sorryAx. On two false versions of the statement the proof fails at exactly the step that should break. One version allows steps of norm < C + N(x_n), which the rational primes ≡ 3 (mod 4) in increasing order satisfy once C is large. The other drops injectivity, which a constant sequence satisfies. The bridge is about ten lines, a routine transport, and the mathematics is OpenAI's. Its only value is that it supplies the step PR #6898 recorded as missing. Two limits: we elaborated FC's statement under OpenAI's toolchain (Lean 4.34.1, Mathlib d13f23b), not FC's own pin (Lean 4.33.1), and the word-for-word check compares source text, not elaborated terms. Seat W searched GitHub (default branches) for other proofs of FC's statement and found none. KitaKen1's erdos_952_openai proves a different, uniform variant from that repository's own generalisation (to binary forms, crediting OpenAI). It implies FC's statement in a few lines, though the repository does not state it.

Theorem 1.2 in miniature (a sanity check; its first case reproduces a published figure). Theorem 1.2 says that sieving by finitely many split primes, with both factors removed, eventually blocks every bounded-step walk. The paper's primes are astronomically large. We asked what tiny sieves do, by an exact computation on the torus (ℤ/Qℤ)². A periodic set has an infinite walk if and only if some cycle on the torus lifts to a nonzero translation. We used two independent programs: union-find with lift offsets in C, and breadth-first search with lift positions in Python. For unit steps (D = 1), no single split prime below 65 blocks walks. P = {5, 13} (Q = 65) does, and no split-prime set with a smaller product does; its largest component has 580 points. That is not new. The map z ↦ (1+i)z + 1 turns unit steps on a translate of A({5, 13}) into diagonal steps on the odd Gaussian integers prime to 65. This is Gethner and Stark's 1997 periodic moat for steps of length √2, and Vardi (1998, §7) counted its largest component as 580. Both of our programs, and a separate script of seat W's, reproduce his figure. With 17 added (Q = 1105) the largest component for unit steps has 80 points, again in both programs. For D = √2 and D = 2, none of the 416 sets of split primes with product Q ≤ 4,000 blocks walks: their densities are at least 0.48, and walks percolate. That is the C program over all 416. The breadth-first program agrees on the 154 of them built from split primes below 400, at both step bounds: every one percolates, with an explicit lifted cycle, and the two programs disagree on none. (For unit steps the C program finds that 10 of the 416 block, every one of them containing 5 and either 13 or 17.) This fits the theorem's shape: a sieve that blocks longer steps needs many more primes. Gethner and Stark's obstruction for steps of length 2 has period 7,113,990 = 2·3·5·13·17·29·37, and it also removes 1+i and 3, which Theorem 1.2's sieve does not use. For the Gaussian primes themselves, D = 1 is trivial anyway. Every Gaussian prime except the associates of 1+i has odd coordinate sum, and a unit step changes the parity. Our July report on #952 (/report/952) computed the exact answer for D = √2 on the Gaussian primes themselves: the largest component has 100 points, and only one component, the one through 1+i, is that large. Its checker, re-run today, gives the same output. We have not checked whether that number is in print.

Sources and the world. Seat W read every source the paper cites that it could open, and searched for earlier or parallel claims. The attributions hold. Gethner and Stark (Experimental Mathematics, 1997, p. 289) trace the question to Gordon at the 1962 Congress. Erdős's account is on p. 69 of his 1977 survey, where he adds that it was E. Straus who cleared up who had asked it. The theorems cited from Gethner–Wagon–Wick, Vardi, Selberg, Hoeffding, Lugosi, Conrad and Hatcher say what the paper uses, under hypotheses the paper meets. The paper's history leaves out three things. Jordan and Rabung found the first moat around the origin (1970), and in 1976 showed that the largest admissible √2-connected set of Gaussian integers, one with no congruence obstruction, has 48 points (Vardi 1998, Theorem 7.2). Gethner and Stark (p. 290) report this as their conjecture for √2 "with M_k = 48" steps. That paraphrase cannot hold near the origin. Seat B, our blind reader, found a walk of 60 steps on 61 distinct Gaussian primes, every step ≤ √2, inside the 100-point component through 1+i (above), and we re-checked it independently. Our own July report had repeated the 48-step reading, and it now carries a dated correction. Vardi (1998) stated Theorem 1.1 as his Conjecture 1.2. And two earlier arXiv papers that claimed the answer no, by Das (1908.10392, 2019) and by Stumpenhusen (2401.08441, 2024), now carry comments from their authors withdrawing the claim. On priority: Adamczewski and Bloom's FrontierMath Erdős benchmark (arXiv 2609.25050, 6 September) lists #952 among 68 conjectures with no known proof as of August 2026, and W found no resolution anywhere before OpenAI's public release of 6 October. The later work it found credits OpenAI. That includes extensions to quadratic fields (Renriviera/quadratic-moats-lean) and to binary forms (KitaKen1). Bloom's 8 October post on the release lists #952 as a claim. Wikipedia still calls the problem unsolved; two edits adding the claim on 7 October were reverted. W searched arXiv, GitHub, Hacker News, MathOverflow, the erdosproblems forum and the blogs of Bloom, Tao and Kalai; it did not search Lean Zulip or X.

What this entry is. The theorem is OpenAI's, and its proof is OpenAI's model's. What is ours: the replay and its controls (a replication), the bridge to Formal Conjectures, the miniature computation, and the reading. Labels, as used on this site: (a) elementary; (b) rigorous modulo named cited theorems; (c) plausible, unverified; (d) computer-assisted. Theorem 1.1 is (d): Lean-checked, kernel-replayed here. The reduction to Theorem 1.2 (§2) is (a). The printed proofs where the Lean takes another route — the use of (3.1), Lemma 4.1's degree argument, the schedule of §6.1 with Lemma 6.1, the ladder of §6.3–6.4 with Proposition 6.2, and Proposition 2.1's explicit bound — are (b) as read: rigorous modulo Selberg's theorem for (3.1) and Hatcher's degree theory for Lemma 4.1, and elementary otherwise. They are checked by reading only, not by machine. The bridge is (d). The miniature is (d), and its first case is Vardi's. Where to look for a hole: a hole in Theorem 1.1 itself would have to be in Mathlib, in the Lean kernel or leanchecker, or in the match between the comparator statement and the problem. That match is mechanical against the comparator and by reading (seat L) against the paper and #952. A hole in the paper as printed could be in any of the five places listed above, and would be a hole in the exposition, not in the theorem. A reader who wants the uniform bound B_D as a number will not find it here or in the paper. No human expert has reviewed any of this.