erdos_238.variant

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

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.