Erdős problem 218
There are infinitely many indices such that the prime gap at is equal to the prime gap at . This is equivalent to the existence of infinitely many arithmetic progressions of length , see erdos_141.variants.infinite_three.
Sources
FormalConjectures/ErdosProblems/
218.lean
Retained formal statement
The set of indices for which a prime gap is followed by a larger or equal prime gap has a natural density of .
{n | primeGap n ≤ primeGap (n + 1)}.HasDensity (1 / 2)OpenStatement only, no proof