Uniformly bounded components of Gaussian-prime graphs

1 paperLean

Proves the Gaussian moat conjecture: no infinite walk through distinct Gaussian primes can have uniformly bounded steps. More strongly, for every distance bound D, the graph joining Gaussian primes at distance at most D has uniformly bounded finite component sizes, depending only on D, including primes on the coordinate axes.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Bounded-Step Walks on Gaussian Primes

OpenAI · September 26, 2026

We prove the Gaussian moat conjecture: no infinite walk through distinct Gaussian primes can have bounded steps. More strongly, for each fixed finite step bound, the connected components of the Gaussian-prime graph have uniformly bounded size. This bound applies to every starting prime, including primes on the coordinate axes, and is nonexplicit. The proof constructs a finite periodic sieve obstruction using geometric sampling and information-theoretic estimates.

Read PDF Download Source

Cite

@misc{OAI:Bounded-Step-Walks-on-Gaussian-Primes-September-26-2026,
  author = {{OpenAI}},
  title = {{Bounded-Step Walks on Gaussian Primes}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Bounded-Step-Walks-on-Gaussian-Primes-September-26-2026/paper.pdf}{OAI:Bounded-Step-Walks-on-Gaussian-Primes-September-26-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Bounded-Step Walks on Gaussian Primes

Scope

The Gaussian moat problem asks whether an infinite walk through distinct Gaussian primes can have bounded step lengths. The formalized result gives a negative answer for every real step bound \(D\). More strongly, one finite bound depending only on \(D\) limits the size of every connected component of the bounded-step graph and the length of every injective bounded-step walk. Axis primes and all associates are included. No explicit function of \(D\) is supplied.

Comparator links

Result	Comparator statement
Uniform bounds for bounded-step Gaussian-prime walks	GaussianMoat.lean

Scope note on GitHub →