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
Heath-Brown [He00] used Kloosterman sums to prove this for all .
∀ c > 3 / 4, ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445.Erdos445Prop c p nSolvedStatement only, no proof