Skip to content

Erdős problem 4

Start work

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

4.lean

Retained formal statement2 of 2

Rankin's theorem: there exists a positive constant CC such that Erdos4For C holds.

FormalConjectures/ErdosProblems/4.leanErdos4.erdos_4.variants.rankin1 lineExact file
∃ C > 0, Erdos4.Erdos4For C
SolvedStatement only, no proof