---

Claim. The file src/latest/ErdosProblems/Erdos310.lean of Boris Alexeev's lean-proofs repository (added 2026-08-17, pinned at the commit of 2026-09-15) proves the theorem erdos_310: for every $\alpha>0$ there is an integer $C\ge1$ such that, for every $N\ge1$ and every $A\subseteq\{1,\ldots,N\}$ with $|A|\ge\alpha N$, some nonempty $S\subseteq A$ has $\sum_{n\in S}1/n=a/b$ with integers $1\le a\le b\le C$. This is the qualitative answer yes to Problem 310, not the bound $\exp(C/\alpha)$ of Liu and Sawhney's Proposition 1.4. The proof applies bloom_finite_bounded_denominator, a finite form of the Bloom--Mehta bounded-denominator extraction from the repository's UnitFractions development, which gives a subsum $1/d$ with $d$ bounded in terms of $D=4/\alpha$.

Depends on. No page of this wiki.

Claimant and standing. The file's header names Thomas Bloom and Bhavik Mehta as informal authors and Codex and GPT-5.6 Sol as formal authors. Neither informal author published this deduction; its published form is the remark of Liu and Sawhney, whom the file does not name. So the file is recorded as the repository's own proof, not as a formalization of a published claim. The formal-conjectures statement file for the problem points at it through its formal_proof attribute, and the Lean suffix of the site's label refers to it. A statement file is not a proof. This corpus has not built or audited the development, so no formalized evidence is listed and the claim is pending.