Conjectures.io

Number theory

Erdős 233

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

References

No one has attempted this yet.

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-379fc029-erdos233-erdos-233-cc7694db92-formalized-v1
Task commitment
sha256:2ebd85aefa5fa95ab06091a6c1a64a99bd3a985ba3dfacc342880c123242c557

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.