Erdős problem 233 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

233.lean

Retained formal statement2 of 3

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.

Formal proof linked here provided by AlphaProof.

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

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

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.