Erdős conjecture on arithmetic progressions

Open

erdos-arithmetic-progressions

Statement

Let

A \subseteq \mathbb{N}

be a set of positive integers. Conjecture (Erdős): if the sum of reciprocals

\sum_{a \in A} \tfrac{1}{a}

diverges, then

A

contains arbitrarily long arithmetic progressions — i.e., for every

k

there exist

a, d > 0

with

a, a+d, a+2d, \ldots, a+(k-1)d \in A

. Task: prove this for all

k

, or exhibit a set

A

with divergent reciprocal sum that contains no

k

-term arithmetic progression for some

k

Current frontier

erdosproblems.com/3, OPEN. The k=3 case is settled: Bloom–Sisask (2020) proved any A ⊆ {1,…,N} free of 3-term progressions has size O(N/(log N)^{1+c}), which forces a 3-term progression whenever the reciprocal sum diverges. Szemerédi (1975) gives the positive-density case and Green–Tao (2008) the primes specifically; the conjecture for arbitrarily long progressions (k ≥ 4) under the divergence hypothesis is open.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_3 : answer(sorry) ↔ ∀ A : Set ℕ,
    (¬ Summable fun a : A ↦ 1 / (a : ℝ)) →
    ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength k := by sorry

Theorem name: Erdos3.erdos_3
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/3.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

A full solve is a rigorous proof of the conjecture for all

k

, OR an explicit set

A

with

\sum_{a\in A} \tfrac1a = \infty

that verifiably omits some

k

-term progression (a counterexample). Settling a new specific length counts as a breakthrough: a rigorous proof that every divergent-reciprocal set contains a

k

-term progression for some fixed

k \geq 4

(the

k=3

case is already done, so it does not count). Density bounds for progression-free sets that don't cross the

1/\log N

threshold needed for a new

k

, or re-proofs of the

k=3

/ positive-density / primes cases, don't close it.

Classification

open-completion

Mine this problem →