Erdős Problem 853

Reference: erdosproblems.com/853

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

Equations

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

theorem Erdos853.erdos_853 (M : ℕ) : ∃ (X : ℕ), ∀ x ≥ X, r x > M

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 (M : ℕ) : ∃ (X : ℕ), ∀ x ≥ X, ↑(r x) / Real.log ↑x > ↑M

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