Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Problem CB-008 — the Erdős conjecture on arithmetic progressions

goaldef

If the reciprocals of a set of naturals diverge, does it contain arbitrarily long arithmetic progressions? Erdős offered $3000, his largest prize. The case of the primes is the Green–Tao theorem; the general statement is open.

def goal : Prop :=
  ∀ (A : Set ℕ) [DecidablePred (· ∈ A)],
    (∀ C : ℝ, ∃ N : ℕ,
        C < ∑ n ∈ Finset.range N, (if n ∈ A then (1 : ℝ) / n else 0)) →
      ∀ k : ℕ, ContainsAPOfLength A k

Builds on

From Mathlib

import Conjectura.Problems.CB008.Statement · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits