Documentation

FormalConjectures.ErdosProblems.«234»

Erdős Problem 234 #

Reference: erdosproblems.com/234

theorem Erdos234.erdos_234 :
sorry ∃ (f : NNReal), Continuous f ∀ (c : NNReal), {n : | (primeGap n) / Real.log n < c}.HasDensity (f c)

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?