Erdős problem 289

Is it true that, for all sufficiently large $k$ , there exists finite intervals $I_1, \dotsc, I_k \subset \mathbb{N}$ with $|I_i| \geq 2$ for $1 \leq i \leq k$ such that $1 = \sum_{i=1}^k \sum_{n \in I_i} \frac{1}{n}.$

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

289.lean

Retained formal statement1 of 1

Is it true that, for all sufficiently large $k$ , there exists finite intervals $I_1, \dotsc, I_k \subset \mathbb{N}$ with $|I_i| \geq 2$ for $1 \leq i \leq k$ such that $1 = \sum_{i=1}^k \sum_{n \in I_i} \frac{1}{n}.$

FormalConjectures/ErdosProblems/289.leanErdos289.erdos_2896 linesExact file

1True ↔2  ∀ᶠ (k : ℕ) in Filter.atTop,3    ∃ I,4      (∀ (i : Fin k), (I i).1 < (I i).2) ∧5        (∀ (i j : Fin k), i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧6          ∑ i, ∑ n ∈ Finset.Icc (I i).1 (I i).2, (↑n)⁻¹ = 1

OpenStatement only, no proof