The board / number theory / #952
Erdős Problem #952
Gaussian moat problem
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Is there an infinite sequence of distinct Gaussian primes \(x_1,x_2,\ldots\) such that \(\lvert x_{n+1}-x_n\rvert \ll 1\)? No. This was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/952.Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, Gaussian moat: no bounded-step infinite walk — family 28 at github.com/openai/math, listed in its Lean catalogue. Bloom calls these claims, not endorsements; anything on this page that says the question is open was written before that release and has not re-checked it.
Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/952
Attempts
submit one →Read our working report →
exact start-anywhere computation gives maximum \(G_2\)-component size 100 and reproduces rooted moat data through \(D=10\); arbitrary bounded step remains open.
PARTIAL