---

Claim. For a finite real $D$ let $G_D$ be the graph whose vertices are all Gaussian primes (the irreducible elements of $\mathbb Z[i]$, associates and axis primes included) with an edge between distinct $z,w$ exactly when $|z-w|\le D$. Theorem 1.1 of the manuscript Bounded-Step Walks on Gaussian Primes, published by OpenAI in its mathematics release with the author line "OpenAI" (26 September 2026; the release's README says its manuscripts were produced by an internal OpenAI model and come at different stages of verification, not all with Lean formalizations), asserts that every connected component of $G_D$ has at most $B_D$ vertices for some finite $B_D$ depending only on $D$; in particular a sequence of distinct Gaussian primes whose consecutive terms are at distance at most $D$ has at most $B_D$ terms. The question of Problem 952, whether an infinite sequence of distinct Gaussian primes with steps bounded by an absolute constant exists, is therefore answered negatively for every constant and every starting point. The bound $B_D$ is not explicit: the proof fixes $D$ and then takes its scales sufficiently large. The argument has two parts. Theorem 1.2, the finite sieve obstruction, gives for every $D\ge1$ a finite set $\mathcal P_D$ of rational primes $p\equiv1\pmod4$, depending only on $D$, such that the Gaussian integers divisible by neither of the two Gaussian prime factors of any $p\in\mathcal P_D$ contain no infinite sequence of distinct points with steps of length at most $D$; it is proved by contradiction, through an entropy argument in which the walk is fixed and only sampled times are random, so that avoiding zero modulo each selected factor costs information at a rate the walk's total entropy budget cannot pay. Proposition 2.1 turns such a periodic obstruction into an explicit bound on every component of $G_D$, since all but finitely many Gaussian primes lie in the sieved set and that set is periodic. The manuscript's statements are carded, with no step of their proofs checked here, at the library card (result pages Theorem 1.1, Theorem 1.2 and Proposition 2.1).

Acceptance. The claim is accepted on formalized evidence. The corpus's verification built the declaration OAI.GaussianMoat.fullMain of the release's Lean development (module OAI/NumberTheory/GaussianMoat/Main.lean in the linked lean/ folder) and checked its axioms: propext, Classical.choice and Quot.sound only. The comparator challenge ComparatorChallenges/GaussianMoat.lean pins the statement, and the solution's fingerprint matched it. The challenge defines, with only Mathlib imported and no local instances, the graph on irreducible Gaussian integers with an edge when the Euclidean distance of the two points in $\mathbb C$ is at most $D$, and states fullMain as the conjunction of two propositions: MainEndpoint, that for every real $D$ no injective sequence $z:\mathbb N\to\mathbb Z[i]$ with every $z_t$ irreducible has $\operatorname{dist}(z_{t+1},z_t)\le D$ for all $t$; and UniformEndpoint, that for every real $D$ some natural number $B$ bounds the cardinality of every component of the graph and the length of every injective finite walk with steps at most $D$. MainEndpoint is the problem's statement: irreducible and prime coincide in $\mathbb Z[i]$, a Euclidean domain; the coercion to $\mathbb C$ makes the distance Euclidean; injectivity means the terms are distinct; quantifying over every real $D$ covers every constant, and so Erdős's strict bound $<C$; no starting point is fixed; and associates and axis primes are included, so the negative answer also covers any narrower reading. The theorem has no hypotheses and the development declares no axioms beyond the three standard ones. No refereed publication, arXiv version or reviewer independent of the release is recorded, so reviewed and refereed are not listed; the site's label is OPEN.

Formal-conjectures statement. The statement file the problem page records bounds the norm (the squared modulus) of each step by an integer $C$, whereas the comparator bounds the Euclidean distance by a real $D$; a bound on one is a bound on the other, so the two conditions agree in content, and no bridging statement was checked.

Depends on. Nothing beyond the cited manuscript.