Skip to content

Erdős problem 3

Start work

If A⊂NA \subset \mathbb{N} has ∑n∈A1n=∞\sum_{n \in A}\frac 1 n = \infty, then must A contain arbitrarily long arithmetic progressions?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

3.lean

Retained formal statement1 of 1

If A⊂NA \subset \mathbb{N} has ∑n∈A1n=∞\sum_{n \in A}\frac 1 n = \infty, then must A contain arbitrarily long arithmetic progressions?

FormalConjectures/ErdosProblems/3.leanErdos3.erdos_31 lineExact file
True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k
OpenStatement only, no proof