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

Erdős and Straus have proved the existence of some constant $c>0$ such that $-c < k(N)-(e-1)N \ll \frac N {\log N}$

FormalConjectures/ErdosProblems/295.leanErdos295.erdos_295.variants.erdos_straus2 linesExact file

1∃ C > 0,2  ∃ O > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos295.k N) - (Real.exp 1 - 1) * ↑N ∈ Set.Ioc (-C) (O * ↑N / Real.log ↑N)

SolvedStatement only, no proof