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 statement1 of 3

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$

Is it true that $\lim_{N \to \infty} k(N) - (e - 1)N = \infty$ ?

FormalConjectures/ErdosProblems/295.leanErdos295.erdos_2951 lineExact file

1sorry ↔ Filter.Tendsto (fun N => ↑(Erdos295.k N) - (Real.exp 1 - 1) * ↑N) Filter.atTop Filter.atTop

OpenStatement only, no proof