Erdős Problem 295

Theorem 295 · Erdős

Helper lemma: for each $N$ , there exists $k$ and $n_1 < ... < n_k$ such that $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$ .

Formal statement · Lean 4.lean

lemma exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k → ℕ),
    (∀ i, N ≤ n i) ∧ StrictMono n ∧ ∑ i, (1 / n i : ℝ) = 1 := by
  sorry

Proof. sorry

Nobody has tried yet.