Does there exist some $c>0$ such that, for any $K>1$, whenever $A$ is a sufficiently large finite multiset of positive integers with ${\sum }_{n\in A}\frac{1}{n}>K$ there exists some $S\subseteq A$ such that$$1-e^{-cK}<\sum _{n\in S}\frac{1}{n}\le 1?$$

A proven wall: An exponential-rate "dense subset-sum near 1" theorem: a constant c>0 such that every sufficiently large finite multiset A of positive integers with R(A)=Σ_{n∈A}1/n > K admits a sub-multiset S with reciprocal sum in (1−e^{−cK}, 1]. Equivalently, prove the best under-approximation satisfies ε(A) := min{1−R(S) : S⊆A, R(S)≤1} ≤ e^{−c·R(A)}. The precise missing input is the IMPROVEMENT of the Erdős–Graham polynomial bound ε(A) ≤ c/K² (known) to an EXPONENTIAL bound ε(A) ≤ e^{−cK}. The bottleneck is a structural lemma showing the achievable sub-sums of A form an exponentially fine net just below 1 — e.g. via a probabilistic/Fourier-analytic concentration argument controlling the granularity of partial reciprocal sums, robust to multiset multiplicities (the primorial construction A=⋃_{p≤N}{p^{(p−1)}} caps the rate at e^{−(1+o(1))K log K}, so the target exponent is essentially optimal in order).

number theory · open · formalized (Lean) · 1 attempt

machinery: egyptian-unit-fractions,subset-sum-density,reciprocal-sum,probabilistic-method,fourier-analytic-method,prime-distribution,primorial-construction