theorem
Erdos952.erdos_952 :
∃ (x : ℕ → GaussianInt) (C : ℤ), Function.Injective x ∧ ∀ (n : ℕ), Prime (x n) ∧ Zsqrtd.norm (x (n + 1) - x n) < C
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$?