Erdős Problem 853

Reference: erdosproblems.com/853

noncomputable def Erdos853.r (x : ℕ) : ℕ

Equations

• Erdos853.r x = sInf {t : ℕ | 0 < t ∧ t % 2 = 0 ∧ ¬∃ n ≤ x, primeGap n = t}

theorem Erdos853.erdos_853 : Filter.Tendsto r Filter.atTop Filter.atTop

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) \to \infty$?

theorem Erdos853.erdos_853_strong : Filter.Tendsto (fun (n : ℕ) => ↑(r n) / Real.log ↑n) Filter.atTop Filter.atTop

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