Erdős problem 3 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

3.lean

Retained formal statement1 of 1

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

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