Source labels openChecked July 26, 2026

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

Number theory AMS 11

Mathematical statement

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

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_289

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_289 : answer(sorry) ↔    (∀ᶠ k : ℕ in atTop, ∃ I : Fin k → ℕ × ℕ,    (∀ i, (I i).1 < (I i).2) ∧    (∀ i j, i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧    ∑ i, ∑ n ∈ .Icc (I i).1 (I i).2, (n⁻¹ : ℚ) = 1) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/289background