Skip to content

Erdős problem 285

Let f(k)f(k) be the minimal value of nkn_k such that there exist n1<n2<⋯<nkn_1 < n_2 < \dots < n_k with 1=1n1+⋯+1nk. 1 = \frac{1}{n_1} + \cdots + \frac{1}{n_k}. Is it true that f(k)=(1+o(1))ee−1k? f(k) = (1 + o(1)) \frac{e}{e - 1} k ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

285.lean

Retained formal statement1 of 2

Let f(k)f(k) be the minimal value of nkn_k such that there exist n1<n2<⋯<nkn_1 < n_2 < \dots < n_k with 1=1n1+⋯+1nk. 1 = \frac{1}{n_1} + \cdots + \frac{1}{n_k}. Is it true that f(k)=(1+o(1))ee−1k? f(k) = (1 + o(1)) \frac{e}{e - 1} k ?

Proved by Martin [Ma00].

[Ma00] Martin, Greg, _Denser Egyptian fractions_. Acta Arith. (2000), 231-260.

FormalConjectures/ErdosProblems/285.leanErdos285.erdos_2857 linesExact file
True ↔  ∀ (f : ℕ → ℕ) (S : Set ℕ),    S = {k | ∃ n, StrictMono n ∧ 0 ∉ Set.range n ∧ 1 = ∑ i, 1 / ↑(n i)} →      (∀ k ∈ S,          IsLeast {x | ∃ n, ∃ (_ : StrictMono n) (_ : 0 ∉ Set.range n) (_ : 1 = ∑ i, 1 / ↑(n i)), n (Fin.last k) = x}            (f k)) →        ∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ k ∈ S, ↑(f k) = (1 + o k) * Real.exp 1 / (Real.exp 1 - 1) * (↑k + 1)
SolvedStatement only, no proof