Erdős Problem 233

References:

• erdosproblems.com/233
• A074741
• Wikipedia

noncomputable def primeGap (n : ℕ) : ℕ

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

Equations

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

theorem sum_of_squares_of_prime_gaps_lower_bound : (fun (N : ℕ) => ↑N * Real.log ↑N ^ 2) =O[Filter.atTop] fun (N : ℕ) => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2

The prime number theorem immediately implies a lower bound of $\gg N(\log N)^2$ for the sum of squares of gaps between consecutive primes.

theorem erdos_233 : (fun (N : ℕ) => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun (N : ℕ) => ↑N * Real.log ↑N ^ 2

A conjecture by Heath-Brown: The sum of squares of the first $N$ gaps between consecutive primes behaves like $N * (log N)^2$.

theorem erdos_233.variant (h : RiemannHypothesis) : (fun (N : ℕ) => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun (N : ℕ) => ↑N * Real.log ↑N ^ 4

Cramér proved an upper bound of $O(N(\log N)^4)$ conditional on the Riemann hypothesis.