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}.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/289.lean

Formal Conjectures

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

Continue