Erdős problem 289
Is it true that, for all sufficiently large , there exists finite intervals with for such that
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/289.leanTrue ↔ ∀ᶠ (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)⁻¹ = 1OpenStatement only, no proof