Erdős problem 853

Let $d_n = p_{n+1} - p_n$ , where $p_n$ is the $n$ th prime. Let $r(x)$ be the smallest even integer $t$ such that $d_n = t$ has no solutions for $n \le x$ .

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

853.lean

Retained formal statement2 of 2

Let $d_n = p_{n+1} - p_n$ , where $p_n$ is the $n$ th prime. Let $r(x)$ be the smallest even integer $t$ such that $d_n = t$ has no solutions for $n \le x$ .

Is it true that $r(x) / \log x \to \infty$ ?

FormalConjectures/ErdosProblems/853.leanErdos853.erdos_853.parts.ii1 lineExact file

1Filter.Tendsto (fun n => ↑(Erdos853.r n) / Real.log ↑n) Filter.atTop Filter.atTop

OpenStatement only, no proof