Erdős problem 445
Is it true that, for any , if is a sufficiently large prime then, for any , there exist such that ?
Sources
FormalConjectures/ErdosProblems/
445.lean
Retained formal statement
Is it true that, for any , if is a sufficiently large prime then, for any , there exist such that ?
This is discussed in this MathOverflow question [MathOverflow].
True ↔ ∀ c > 1 / 2, ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445.Erdos445Prop c p nOpenStatement only, no proof