Erdős problem 952 · problems.science

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$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

952.lean

Retained formal statement1 of 1

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$ ?

FormalConjectures/ErdosProblems/952.leanErdos952.erdos_9521 lineExact file

1∃ x C, Function.Injective x ∧ ∀ (n : ℕ), Prime (x n) ∧ Zsqrtd.norm (x (n + 1) - x n) < C

OpenStatement only, no proof