Erdős problem 238
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₂?
Sources
FormalConjectures/ErdosProblems/
238.lean
Retained formal statement
It is well-known that the conjecture above is true when c₁ is sufficiently small.
∀ c₂ > 0, ∀ᶠ (c₁ : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ᶠ (x : ℝ) in Filter.atTop, ∃ k, c₁ * Real.log x < ↑k ∧ ∃ f m, (∀ (i : Fin k), ↑(f i) ≤ x ∧ f i = Nat.nth Nat.Prime (m + ↑i)) ∧ ∀ (i : Fin (k - 1)), c₂ < primeGap (m + ↑i)SolvedStatement only, no proof