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

Conjectura.Problems.CB008.Statement

/-
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
-/
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Conjectura.Defs.Mathematics.Combinatorics.ArithmeticProgression

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

LOCKED: solvers cannot modify this file.
-/
namespace Conjectura.CB008
open Conjectura.Combinatorics
/-- 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
end Conjectura.CB008