Erdős problem 312

Does there exist a constant `c > 0` such that, for any `K > 1`, whenever `A` is a sufficiently large finite multiset of integers with $\sum_{n \in A} 1/n > K$ there exists some $S \subseteq A$ such that $1 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

312.lean

Retained formal statement1 of 1

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with $\sum_{n \in A} 1/n > K$ there exists some $S \subseteq A$ such that $1 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1$ ?

FormalConjectures/ErdosProblems/312.leanErdos312.erdos_3129 linesExact file

1True ↔2  ∃ c,3    0 < c ∧4      ∀ (K : ℝ),5        1 < K →6          ∃ N₀,7            ∀ (n : ℕ) (a : Fin n → ℕ),8              n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K →9                ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1

OpenStatement only, no proof