Erdős problem 234
Is it true that for all c ≥ 0, the density f c of integers for which (p (n + 1) - p n) / log n < c exists and is a continuous function of c?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/234.leanTrue ↔ ∃ f, Continuous f ∧ ∀ (c : NNReal), {n | ↑(primeGap n) / Real.log ↑n < ↑c}.HasDensity (f c)OpenStatement only, no proof