The Gaussian moat problem asks whether there is an infinite sequence of distinct Gaussian primes 
and a fixed real number 
such that 
for every 
(Gethner et al. 1998). Equivalently, for some 
the graph
joining Gaussian primes at distance
at most 
would have an infinite connected component.
The equivalence uses the fact that bounded regions contain only finitely many Gaussian integers.
OpenAI (2026) gave a Lean-formalized proof that the answer is negative. More strongly, for every fixed 
, there is a finite bound depending
only on 
for the size of every connected component
of this graph. The bound includes Gaussian
primes on the coordinate axes and all their associates,
and is not explicit. Gethner et al. (1998) showed that for 
the connected
component containing 
is finite. Such a finite moat
by itself does not exclude an infinite connected
component elsewhere. This is the Gaussian-prime version of the moat-crossing
problem.
This is problem 952 in the Erdős problems collection (Bloom 2026).
