erdős #952 · Gaussian moat problem
Is there an infinite sequence of distinct Gaussian primes such that
Worked, still open.
number theory · open · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Your question is exactly the **Gaussian moat problem**: view the Gaussian primes as vertices in a graph, connect two primes if their Euclidean distance is at most some fixed constant $C$, and ask whether there is an **infinite path** [[nomath]](equivalently, an infinite sequence $x_1,x_2,\dots$ of distinct Gaussian pri…
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_952 :
∃ (x : ℕ → GaussianInt) (C : ℤ),
Function.Injective x ∧
∀ n, Prime (x n) ∧ (x (n + 1) - x n).norm < Cformal-conjectures/952.lean ↗links
Gaussian moat problem · reference
status
open