Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. For every and every large in terms of , every with has a subset with . 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 such that, for all large , every with
contains with reciprocal sum one. For fixed the right side is below once , so the hypothesis 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 with no unit subsum, which lies between (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
, 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.