---

Claim. Theorem 2 of arXiv v2 (Theorem 1.2 of the published version): if $A\subseteq\mathbb N$ satisfies

$$\limsup_{N\to\infty}\frac{|A\cap[1,N]|}N>0,$$

then some finite $S\subseteq A$ has $\sum_{n\in S}1/n=1$. A set of positive density in any reading the problem page's Formulation lists (natural, lower or upper density) has positive upper density, so the answer to the question is yes in every reading; the hypothesis needed is the weakest one, and the natural density need not exist. Theorem 2 is derived directly from the paper's Proposition 1. Theorem 3 of arXiv v2 (Theorem 1.3 of the published version), proved by the same method, gives a quantitative criterion for the logarithmic-density analogue: for an absolute constant $C$ and large $N$, a set $A\subseteq\{1,\ldots,N\}$ with $\sum_{n\in A}1/n\ge C\log N\log\log\log N/\log\log N$ has a unit subsum.

Acceptance. The paper is refereed: On a density conjecture about unit fractions, Journal of the European Mathematical Society 27 (2025), no. 11, 4563–4589, first online 11 July 2024; the arXiv preprint was first posted on 7 December 2021 and revised on 12 October 2023. The site's curator, Thomas Bloom, is the theorem's author, so the site's label, PROVED (LEAN), is recorded here as the catalog's label and not as independent review. The library compiles the proof from Theorem 2 down through its lemmas and propositions, using at Proposition 1 the variant of the printed criterion that the formalization proves, since the printed parameters do not match the printed proof; this compilation detail does not change the result.

Formalization. Appendix B of the paper, written by Bloom and Bhavik Mehta, reports a complete Lean 3 verification of the theorem; the linked declaration unit_fractions_upper_density is the author's own formalization and is pinned to the development's commit. This corpus has not built or audited it, so it is a posting of the result and gives no formalized evidence here. Two Lean 4 postings of the same formalization are linked above: the file src/latest/ErdosProblems/Erdos298.lean of Boris Alexeev's lean-proofs collection, which declares itself a formalization of Bloom's solution, names Bloom as informal author and Mehta and Bloom as formal authors, and proves erdos_298 and erdos_298_density from unit_fractions_upper_density, recording the axioms propext, Classical.choice and Quot.sound; and a vendored single-file copy of the Lean 4 port in Jayyhk/erdos-lean. The corpus has built neither. The formal-conjectures file for the problem states the upper-density and natural-density versions with sorry bodies and tags the Bloom–Mehta development as the external proof; it is a statement file, not a formalization link.

Consequences and refinements. The theorem disproves the bounded-gap sequence of Problem 299, recorded as its own claim page. Liu and Sawhney's later Theorem 1.1 lowers the reciprocal-mass threshold to $(\log N)^{4/5+\varepsilon}$; it is a refinement of Theorem 3, recorded on the problem page, and that threshold is the subject of Problem 47, where it is the accepted claim page Liu and Sawhney's four-fifths threshold.