Erdős problem 3

If $A \subset \mathbb{N}$ has $\sum_{n \in A}\frac 1 n = \infty$ , then must A contain arbitrarily long arithmetic progressions?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/3.lean

Formal Conjectures

FormalConjectures/ErdosProblems/3.leanErdos3.erdos_31 lineExact file

1True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k

OpenStatement only, no proof