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 ?$

unreviewedOpen. Worked here; no verified result yet.

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

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

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Formal proof

AMS 11 · solved (literature)

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

OEIS1

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela