OpenFrontiers
Join
← Back to the index
OP-8895OpenNumber theory

Erdős #233 · number theory / primes

Let dn=pn+1−pnd_n=p_{n+1}-p_n, where pnp_n is the nnth prime. Prove that

∑1≤n≤Ndn2≪N(log⁡N)2.\sum_{1\leq n\leq N}d_n^2 \ll N(\log N)^2.
MSC 11 · Number theory

Inferred from the community field; finer classification has not been reviewed.

Source reports OPENAs of 2026-09-08Source & evidence ↓
Read original source ↗ 0Submit progressLean 4 ↓Discussion (0)

Problem statement

Let dn=pn+1−pnd_n=p_{n+1}-p_n, where pnp_n is the nnth prime. Prove that

∑1≤n≤Ndn2≪N(log⁡N)2.\sum_{1\leq n\leq N}d_n^2 \ll N(\log N)^2.

Lean 4

No Lean submitted

Formal statement

The formalization is available at the source below; its code is not attached here yet.

On-site verification needs an executable Lean target. None is attached yet.

A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.

Proofs & verification

No Lean has been submitted for this problem yet. A Lean file can be attached to a submission for review, though with no target here it cannot be machine-checked.

Share a formalization →Verification guide ↗

Background

Cramer [Cr36] proved an upper bound of O(N(log⁡N)4)O(N(\log N)^4) conditional on the Riemann hypothesis. Selberg [Se43] improved this slightly (still assuming the Riemann hypothesis) to

∑1≤n≤Ndn2n≪(log⁡N)4.\sum_{1\leq n\leq N}\frac{d_n^2}{n}\ll (\log N)^4.

The prime number theorem immediately implies a lower bound of

∑1≤n≤Ndn2≫N(log⁡N)2.\sum_{1\leq n\leq N}d_n^2\gg N(\log N)^2.

This would imply in particular that dn≪n1/2log⁡nd_n\ll n^{1/2}\log n for all nn, which is known only the assumption of the Riemann Hypothesis.

The values of the sum are listed at A074741 on the OEIS.

This is discussed in problem A8 of Guy's collection [Gu04].

Progress & source assessment

The source labels this entry OPEN in the 2026-09-08 snapshot. Editorial progress notes are reproduced as source commentary, not independently verified results. Prize amounts and Lean badges at the source are not local awards or verification.

References
  1. [1]Thomas Bloom (ed.), Erdős Problems #233 link
  2. [2]Upstream Lean 4 statement for Erdős #233 linkExternal statement reference. Not compiled or verified by this platform; upstream files may contain open proof obligations.
  3. [3]Formal Conjectures — Erdős Problem 233 link

Recorded progress

Add yours →

Nothing recorded yet. A pointer to a paper the entry is missing counts.

Machine attempts

0 recorded

Attempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.

No machine attempts recorded.

Sign in to run an attempt. New accounts start with enough credits for ten.

Discussion

0 notes

Notes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.

No notes yet.

Sign in to add a note.