Erdős Problem 4

Reference: erdosproblems.com/4

def Erdos4For (C : ℝ) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem erdos_4 : (∀ C > 0, Erdos4For C) ↔ True

Is it true that, for any $C > 0$, there infinitely many $n$ such that: $$ p_{n + 1} - p_n > C \frac{\log\log n\log\log\log\log n}{(\log\log\log n) ^ 2}\log n $$

theorem erdos_4.variants.rankin : ∃ C > 0, Erdos4For C