Erdős Problem 218

Reference: erdosproblems.com/218

noncomputable def Erdos218.primeGap (n : ℕ) : ℕ

The prime gap: the difference between the $n+1$-th and $n$-th prime.

Equations

• Erdos218.primeGap n = Nat.nth Nat.Prime (n + 1) - Nat.nth Nat.Prime n

theorem Erdos218.erdos_218.variants.le : {n : ℕ | primeGap n ≤ primeGap (n + 1)}.HasDensity (1 / 2)

The set of indices $n$ for which a prime gap is followed by a larger or equal prime gap has a natural density of $\frac 1 2$.

theorem Erdos218.erdos_218.variants.ge : {n : ℕ | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

The set of indices $n$ for which a prime gap is preceeded by a larger or equal prime gap has a natural density of $\frac 1 2$.

theorem Erdos218.erdos_218.variants.infinite_equal_prime_gap : {n : ℕ | primeGap n = primeGap (n + 1)}.Infinite

There are infintely many indices $n$ such that the prime gap at $n$ is equal to the prime gap at $n+1$. This is equivalent to the existence of infinitely many arithmetic progressions of length $3$, see erdos_141.variant.infinite_three.