Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. For every δ>0\delta>0 and every NN large in terms of δ\delta, every A⊆{1,…,N}A\subseteq\{1,\ldots,N\} with ∑a∈A1/a>δlog⁡N\sum_{a\in A}1/a>\delta\log N has a subset SS with ∑n∈S1/n=1\sum_{n\in S}1/n=1. The answer to Problem 47 is yes.

Result. Bloom's Theorem 3 (J. Eur. Math. Soc. 27 (2025), no. 11, 4563--4589, Theorem 1.3 of the published version; arXiv:2112.03726v2, p. 2; paged at theorem_3) gives an absolute constant CC such that, for all large NN, every A⊆{1,…,N}A\subseteq\{1,\ldots,N\} with

∑a∈A1a≥C log⁡log⁡log⁡Nlog⁡log⁡N log⁡N\sum_{a\in A}\frac1a\ge C\,\frac{\log\log\log N}{\log\log N}\,\log N

contains S⊆AS\subseteq A with reciprocal sum one. For fixed δ>0\delta>0 the right side is below δlog⁡N\delta\log N once N≥N0(δ)N\ge N_0(\delta), so the hypothesis ∑a∈A1/a>δlog⁡N\sum_{a\in A}1/a>\delta\log N implies it; this one-line specialization is written on the source card and on the problem page, and the site's commentary records Theorem 3 as the solution. The library holds a complete rewritten proof of Theorem 3 through the explicit variant of the paper's Proposition 1 used by the existing formalization. The theorem leaves open the order of the largest reciprocal sum of a subset of {1,…,N}\{1,\ldots,N\} with no unit subsum, which lies between (log⁡log⁡N)2(\log\log N)^2 (Pomerance's construction, the paper's Theorem 4) and the threshold above; a sharper threshold is the subject of Liu and Sawhney's claim page.

Acceptance. Refereed: the paper appeared in the Journal of the European Mathematical Society (submitted 1 February 2022, accepted 11 October 2023, first online 11 July 2024). The site's curator is the claimant, so the site's label and commentary count as no independent review on this page. The rewritten proof in the library has no independent review.

Formalization. The paper's Appendix B, written with Bhavik Mehta, describes a complete formal verification of the main results in Lean 3; at the pinned commit of their repository, unit_fractions_upper_log_density in src/final_results.lean states Theorem 3. The second linked file, in Lean 4, declares itself a formalization of a solution to Problem 47, names Bloom as its informal author and Mehta and Bloom as its formal authors, restates Theorem 3 and derives from it the statement of the problem with δlog⁡N<∑a∈A1/a\delta\log N<\sum_{a\in A}1/a, without sorry; its recorded axioms are propext, Classical.choice and Quot.sound. This corpus has not built or audited either development, so they are postings of the result and not formalized evidence here; the site's Lean suffix is a catalog label, and the formal-conjectures statement file for the problem carries a sorry body.