we-solve (beta)

Math-639 · mathematics · Number theory

Walking to Infinity on Gaussian Primes

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

The Gaussian integers are ${\mathbb{Z}}[i]$. A Gaussian prime is a nonzero nonunit irreducible element of this ring; associates are allowed as different lattice points. The question asks for $M<\infty$ and an infinite sequence $z_j$ of Gaussian primes, starting within bounded distance of the origin, with $|z_{j+1}-z_j|\leq M$ and $|z_j|\to\infty$. The origin is the starting location, not itself a Gaussian prime. [S1] [S2]

Statement recorded in the supplied source.
Can one walk from the origin to infinity using Gaussian primes as stepping stones and taking steps of bounded length? [S1]
Residual task reported by the archive.

The embedded review (2026-08-17) records: Either drive the path exponent to zero with a uniform constant or prove arbitrarily wide Gaussian-prime moats. [S1]

Short English statement

Can one travel arbitrarily far through Gaussian-prime lattice points without ever needing an unbounded step?

Sources

  • S1 ULAM.AI, UnsolvedMath, supplied problems.json, record 1869 (GUY-A16), statement and background. The embedded literature-review date is 2026-08-17; that is the archive’s review date, not a fresh certification. Dataset landing page: https://huggingface.co/datasets/ulamai/UnsolvedMath.

  • S2 Jori Merikoski (joint work with James Maynard), On the Gaussian moat problem, Oberwolfach Reports 50/2022, 2940-2942. https://ems.press/content/serial-article-files/46986. Bibliographic information from the supplied record.

  • S3 Johann Christian Stumpenhusen, On the Gaussian Moat Problem, arXiv:2401.08441, withdrawn (2024). https://arxiv.org/abs/2401.08441. Bibliographic information from the supplied record.

  • S4 Madhuparna Das, A Note on The Gaussian Moat Problem, arXiv:1908.10392, withdrawn (2024). https://arxiv.org/abs/1908.10392. Bibliographic information from the supplied record.

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-639-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-639

The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting result is manuscript 1 (family 028; 2026-09-26). The manuscript also gives additional strength beyond the requested conclusion; that excess is not required for this problem's solved-claim label.

Walking to Infinity on Gaussian Primes

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 028; 2026-09-26), the asserted result is that for each finite step bound, all connected Gaussian-prime components have a common finite size bound, ruling out infinite injective walks, including those meeting axis primes.

Mathematical statement of the claimed result

Manuscript 1.
For $D<\infty$, form $G_D$ on all Gaussian primes in $\mathbb Z[i]$, joining distinct vertices when their Euclidean distance is at most $D$. The claimed uniform bound is \[ \forall D<\infty\ \exists B_D<\infty\ \forall\text{ connected components }C\subseteq G_D:\quad |C|\le B_D. \] Axis primes are included. Consequently a sequence of distinct Gaussian primes with every successive distance at most $D$ has at most $B_D$ terms; the bound does not depend on its starting point.

Outline of the argument

For manuscript 1 (family 028; 2026-09-26), geometric sampling of a hypothetical long walk produces many residue differences. Shared continuation data create an entropy budget incompatible with avoiding zero residues, yielding a finite periodic sieve barrier and hence the uniform component bound.

Formal verification

For manuscript 1 (family 028; 2026-09-26), OpenAI lists Lean statements for this assertion: for each finite step bound, all connected Gaussian-prime components have a common finite size bound, ruling out infinite injective walks, including those meeting axis primes.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are GaussianMoat.lean.

Their named declarations include OAI.GaussianMoat.fullMain.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →