Erdős problem 285 · problems.science

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/285.lean

Formal Conjectures

FormalConjectures/ErdosProblems/285.leanErdos285.erdos_2857 linesExact file

1True ↔2  ∀ (f : ℕ → ℕ) (S : Set ℕ),3    S = {k | ∃ n, StrictMono n ∧ 0 ∉ Set.range n ∧ 1 = ∑ i, 1 / ↑(n i)} →4      (∀ k ∈ S,5          IsLeast {x | ∃ n, ∃ (_ : StrictMono n) (_ : 0 ∉ Set.range n) (_ : 1 = ∑ i, 1 / ↑(n i)), n (Fin.last k) = x}6            (f k)) →7        ∃ 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

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Continue

Search problems.science