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

Worked, still open.

number theory · solved · prize $10000 · formalized (Lean) · 0 attempts

machinery: prime-distribution,prime-gaps,covering-system,sieve/Brun-Titchmarsh,Maynard-GPY-sieve

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 11 · solved (literature)

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

solved