Number theory · Last catalog review 26 Jul 2026

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

References

Published 3 Jun 2026Never attempted

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«233»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos233.erdos_233" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/233.lean

Source type SHA-256: sha256:c87f57546a66944ad490caa8666193bc1e6a40b09d5d839702cefb6425982be1
Task id: fc-e923379e-erdos233-erdos-233-f97637ffd1-formalized-v1
Task commitment: sha256:d51acb6f4288d5913ede81d5db97716332bc25a0a58deafb236714dc25df989c

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.