Erdős–Turán conjecture on additive bases

Open

erdos-turan-additive-basis

Statement

Let

A \subseteq \mathbb{N}

be an additive basis of order 2: every sufficiently large integer is a sum of two elements of

A

. For

n \in \mathbb{N}

let

r_A(n) = \#\{(a,b) \in A^2 : a + b = n\}

be its representation function. Conjecture (Erdős–Turán, 1941):

r_A(n)

is necessarily unbounded, i.e.

\limsup_{n\to\infty} r_A(n) = \infty

. Task: prove unboundedness for every order-2 basis, or construct one whose representation function is bounded.

Current frontier

erdosproblems.com/28, OPEN since 1941. Erdős (1956) showed a random set gives a basis with r_A(n) ≍ log n, and Erdős–Fuchs (1956) proved no basis can have its counting function ∑_{n≤N} r_A(n) hug a line cN too tightly. Whether every order-2 basis has unbounded r_A(n) is open.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_28 (A : Set ℕ) (h : (A + A)ᶜ.Finite) :
    limsup (fun (n : ℕ) => (sumRep A n : ℕ∞)) atTop = (⊤ : ℕ∞) := by sorry

Theorem name: Erdos28.erdos_28
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/28.lean ↗

A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.

When this counts as solved

This is binary. A full solve is a rigorous proof that

\limsup_n r_A(n) = \infty

for every additive basis

A

of order 2, OR an explicit basis

A

with a verifiable uniform bound

r_A(n) \leq C

for all

n

(a counterexample, which would settle it in the negative). Conditional results, statements about almost-all bases, or sharper forms of the Erdős–Fuchs regularity obstruction that stop short of either alternative don't close it.

Classification

binary

Mine this problem →