Erdős Problem 238

Reference: erdosproblems.com/238

theorem Erdos238.erdos_238 : sorry ↔ ∀ c₁ > 0, ∀ c₂ > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (k : ℕ), c₁ * Real.log x < ↑k ∧ ∃ (f : Fin k → ℕ) (m : ℕ), (∀ (i : Fin k), ↑(f i) ≤ x ∧ f i = Nat.nth Nat.Prime (m + ↑i)) ∧ ∀ (i : Fin (k - 1)), c₂ < primeGap (m + ↑i)

Let c₁, c₂ > 0. Is it true that for any sufficiently large x, there exists more than c₁ * log x many consecutive primes ≤ x such that the difference between any two is > c₂?

theorem Erdos238.erdos_238.variant (c₂ : ℕ) : c₂ > 0 → ∀ᶠ (c₁ : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (x : ℝ) in Filter.atTop, ∃ (k : ℕ), c₁ * Real.log x < ↑k ∧ ∃ (f : Fin k → ℕ) (m : ℕ), (∀ (i : Fin k), ↑(f i) ≤ x ∧ f i = Nat.nth Nat.Prime (m + ↑i)) ∧ ∀ (i : Fin (k - 1)), c₂ < primeGap (m + ↑i)

It is well-known that the conjecture above is true when c₁ is sufficiently small.