The Gaussian moat problem

The Gaussian moat problem asks whether one can walk to infinity through distinct Gaussian primes using steps of bounded length. It is Problem 952 on the Erdős problems site, which notes that the problem is due to Basil Gordon and Motzkin rather than to Erdős. A manuscript dated 26 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a negative answer in a uniform form, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • Gethner and Stark trace the question to Basil Gordon at the 1962 International Congress of Mathematicians in Stockholm. Erdős later credited Gordon and Motzkin, recalling that Motzkin told him the problem at a number theory meeting in Pasadena in November 1963.
  • Large prime-free disks block a walk locally, but a walk in the plane may go around them. Gethner, Wagon and Wick constructed such disks centred on lines and constructed arbitrarily isolated real Gaussian primes, crediting Vardi with an independent proof of the latter. Tsuchimura showed by computation that steps of length at most 6 starting from the origin reach only a bounded distance.
  • Gethner and Stark formulated a bound on walk length that is uniform in the starting point, established periodic obstructions for the step bounds √2 and 2, and proposed sieving by small Gaussian primes for larger bounds. Vardi studied the associated periodic coprimality graphs and the passage from the absence of an infinite walk to a uniform bound on component sizes.
• The Erdős problems page for Problem 952 (accessed 17 October 2026; last edited 8 April 2026) quotes Erdős's 1980 remark that the answer is almost certainly negative, and lists no proof claims.

The original result

• Uniformly bounded components (26 September 2026). Theorem 1.1 of the manuscript states that for every finite real D there is a finite number B_D such that, in the graph on the Gaussian primes joining two primes at distance at most D, every connected component has at most B_D vertices. The bound does not depend on the starting prime and includes primes on the coordinate axes. Consequently no infinite sequence of distinct Gaussian primes has bounded steps. The manuscript states that the bound is not explicit.
  • Method, as described: a finite sieve theorem states that for each step bound there is a finite set of rational primes congruent to 1 modulo 4 such that the Gaussian integers divisible by neither Gaussian factor of any of these primes contain no infinite walk with steps of that length. A periodicity argument converts this into the uniform component bound. The sieve theorem is proved for an arbitrary self-avoiding walk by geometric sampling, entropy and coverage estimates for residues, and an information budget that the manuscript relates to Tao's entropy-decrement argument.
• Sources. Commit 1581d4c of the openai/math repository, folder Bounded-step walks on Gaussian primes.
• Formalization, as described by the repository. The scope note lean/docs/028.md states that the formalization gives a negative answer for every real step bound. One finite bound depending only on the step bound limits the size of every connected component and the length of every injective bounded-step walk. Axis primes and all associates are included, and no explicit function of the step bound is supplied. The Comparator statement is GaussianMoat.
• Kernel records. In the con-leche development journal's run over all 416 Comparator challenges of the collection (repository commit fd4aeeb, run of 10 October 2026; DESIGN.md, task #348), con-leche and Lean's official kernel both accepted 401 challenges; GaussianMoat is not among the 15 named exceptions.
• Catalogue status. In Formal Conjectures, the statement of Erdős Problem 952 is marked solved on the main branch, with a formal proof link to the openai/math Lean file at commit adc7f12 (ErdosProblems/952.lean).

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-07	Renriviera/quadratic-moats-lean (GitHub)	Extension (Lean)	Lean proofs that, for every quadratic number field and every step bound, the graph on the irreducible elements of its ring of integers, with distances measured in the Minkowski embedding, has connected components of uniformly bounded size. A second theorem gives the same conclusion for the nonzero elements whose principal ideals have at most b distinct prime ideal factors. Real and imaginary quadratic fields are both covered, including rings of integers without unique factorization. The repository follows the OpenAI formalization and retains its modules.	Repository with Lean 4.34.1. The README reports a local build of 9 October 2026 with only the standard axioms, and a GitHub Actions workflow that builds and audits both theorems.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the GaussianMoat solution (458 s).	Repository.
2026-10-10	Kenta Kitamura (GitHub KitaKen1), erdos-952-binary-form-moat-classification	Extension (Lean)	Lean proofs for binary forms. Let F be an irreducible homogeneous polynomial in two variables with integer coefficients and degree at least 2, and consider the lattice points at which F is nonzero and its absolute value has at most r distinct prime divisors. For each step bound, the graph on these points has connected components of uniformly bounded size. A classification states that, for a nonzero homogeneous form of positive degree, arbitrarily long walks of this kind exist for some step bound and some r exactly when the form is a constant multiple of a power of a linear form. The repository also states the uniform Gaussian variant in the style of Formal Conjectures.	Repository; the Lean project uses Lean v4.35.0-rc3.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.