Erdős Problem #952
Gaussian moat problem

Read our full write-up →

Can you walk to infinity on the Gaussian primes if every step has bounded length? Gethner and Stark trace the question to Basil Gordon in 1962; it has been attributed to Erdős, who wrote that the answer is almost certainly no. OpenAI's preprint, dated 26 September and public since 6 October, proves the answer is no, in the uniform form that Gethner and Stark conjectured in 1997: for every step bound D there is a number B_D, never computed, such that every connected component of the Gaussian primes joined at distance at most D has at most B_D points. OpenAI's Lean proof (41 modules, importing only Mathlib) compiles on our machine on the three standard axioms, as it already had for at least three others in October, and its statement prints identically to the comparator statement the release designates. Five AI referee seats, each briefed to refute one part, read the paper, its sources and its Lean; none found a gap or an error. In four places the Lean takes a different route from the paper. Ours: a Lean proof of Formal Conjectures' erdos_952, derived from OpenAI's theorem. FC marks the problem solved but its proof is still sorry, and the FC pull request that marked it recorded the norm-to-distance step as not in the linked proof. A script checks our copy of FC's statement word for word. We add a uniform version in FC's vocabulary, and a small exact computation of the paper's sieve statement whose first case reproduces a 1998 figure of Vardi's. None of this has been reviewed by a human expert.