erdős #6
Let . Are there infinitely many such that ?
unreviewedOpen. Worked here; no verified result yet.
number theory · solved · prize $100 · formalized (Lean) · 0 attempts
machinery: prime-distribution,sieve/Brun-Titchmarsh,Hardy-Littlewood,consecutive-integer-window
use this data
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsFormal proof
AMS 11 · solved (literature)
theorem erdos_6 :
{n | primeGap n < primeGap (n + 1) ∧ primeGap (n + 1) < primeGap (n + 2)}.Infiniteformal-conjectures/6.lean ↗OEIS1
Check it yourself
One command re-derives this record's receipts on your machine.
vela reproduce examples/erdos-problems