Skip to content

Erdős problem 289

Is it true that, for all sufficiently large kk, there exists finite intervals I1,…,Ik⊂NI_1, \dotsc, I_k \subset \mathbb{N} with ∣Ii∣≥2|I_i| \geq 2 for 1≤i≤k1 \leq i \leq k such that 1=∑i=1k∑n∈Ii1n. 1 = \sum_{i=1}^k \sum_{n \in I_i} \frac{1}{n}.

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

289.lean

Retained formal statement1 of 1

Is it true that, for all sufficiently large kk, there exists finite intervals I1,…,Ik⊂NI_1, \dotsc, I_k \subset \mathbb{N} with ∣Ii∣≥2|I_i| \geq 2 for 1≤i≤k1 \leq i \leq k such that 1=∑i=1k∑n∈Ii1n. 1 = \sum_{i=1}^k \sum_{n \in I_i} \frac{1}{n}.

FormalConjectures/ErdosProblems/289.leanErdos289.erdos_2896 linesExact file
True ↔  ∀ᶠ (k : ℕ) in Filter.atTop,    ∃ I,      (∀ (i : Fin k), (I i).1 < (I i).2) ∧        (∀ (i j : Fin k), i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧          ∑ i, ∑ n ∈ Finset.Icc (I i).1 (I i).2, (↑n)⁻¹ = 1
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page