Let $d_{n} = p_{n + 1} - p_{n}$ , where $p_{n}$ is the $n$ th prime. Prove that $1 \leq n \leq N \sum d_{n}^{2} ≪ N (lo g N)^{2} .$

unreviewedOpen. Worked here; no verified result yet.

number theory · open · formalized (Lean) · 0 attempts

Check This Result Yourself

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is a famous **Erdős problem** (Erdős Problem #233), and **the bound you ask for is currently open** (i.e., no proof is known as of the latest references I can find). ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

Formal proof

AMS 11 · open (literature)

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

formal-conjectures/233.lean ↗

OEIS1

A074741 — Sum of squares of gaps between consecutive primes.1,5,9,25,29,45,49,65,101,105,141,157,161,177,213,249,253,289,305,309,345,361,397,461,477,481,497,501,517,713,729,765,769

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela