Erdős problem 233

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

233.lean

Retained formal statement3 of 3

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

FormalConjectures/ErdosProblems/233.leanErdos233.erdos_233.variants.upper_bound1 lineExact file

1RiemannHypothesis → (fun N => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun N => ↑N * Real.log ↑N ^ 4

SolvedStatement only, no proof