Erdős Problem 233

Conjecture 233 · Erdős

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

Formal statement · Lean 4.lean

theorem erdos_233 :
    (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ)) =O[atTop] fun N => N * (log N)^2 := by
  sorry

Proof. sorry

Nobody has tried yet.