Erdős problem 295

Let $k(N)$ denote the smallest $k$ such that there exists $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

295.lean

Retained formal statement3 of 3

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

FormalConjectures/ErdosProblems/295.leanErdos295.exists_k1 lineExact file

1∀ (N : ℕ), ∃ k n, (∀ (i : Fin k.succ), N ≤ n i) ∧ StrictMono n ∧ ∑ i, 1 / ↑(n i) = 1

TextbookStatement only, no proof