Proved. The status-defining source is Liu and Sawhney's Proposition 1.4 (Int. Math. Res. Not. 2026, refereed): there is an absolute $C\ge1$ such that for $\varepsilon>0$, $N$ large in terms of $\varepsilon$, $A\subseteq[1,N]$ with $|A|\ge\alpha N$ and $(\log N)^{-1/7+\varepsilon}\le\alpha\le1/2$, some $B\subseteq A$ has $\sum_{n\in B}1/n=s/t$ with $1\le s\le t\le\exp(C/\alpha)$; for $\alpha>1/2$ the case $\alpha=1/2$ applies to any subset of $A$ of size $N/2$ (checked on this page). The site attributes the qualitative answer to Bloom's density theorem through Liu and Sawhney's observation; their remark says a direct application of Bloom's Proposition 1 gives $t=O_\alpha(1)$, and that the dependence $\exp(O(1/\alpha))$ is sharp. The site's label is PROVED (LEAN); its Lean suffix refers to a Lean development in Boris Alexeev's collection, authored by OpenAI Codex and naming Thomas Bloom and Bhavik Mehta as its informal authors, at which the formal-conjectures statement file added on 20 September 2026 points; it proves the qualitative answer by the route of Bloom's density theorem, has its own pending claim page, Alexeev's Lean proof, and is described under Existing formalization, and no local kernel credit is claimed. The accepted claim is recorded on Liu and Sawhney's claim page (2024).