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₂?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/238.leanTrue ↔ ∀ c₁ > 0, ∀ c₂ > 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)OpenStatement only, no proof