Erdős Problem 3

Reference: erdosproblems.com/3

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

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