---

Claim. No infinite sequence $a_1<a_2<\cdots$ of positive integers with $a_{i+1}-a_i=O(1)$ avoids a finite sum of distinct reciprocals equal to one. If $a_{i+1}-a_i\le H$ for all $i\ge i_0$, then $|\{a_i\}\cap[1,N]|\ge1+\lfloor(N-a_{i_0})/H\rfloor$ for $N\ge a_{i_0}$, so the set of values has lower density at least $1/H$ and in particular positive upper density. Bloom's Theorem 2 of arXiv v2 (Theorem 1.2 of the published version) then gives a finite set of values with reciprocal sum one, and the indices of those values, distinct because the sequence is strictly increasing, give the required finite sum. The answer to the question is no.

Depends on. Bloom's positive-upper-density theorem supplies the whole argument beyond the counting inequality above.

Acceptance. The density theorem 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, first posted to arXiv on 7 December 2021. The bounded-gap consequence is not a numbered result of the paper; the site's commentary identifies it as following from the positive solution of Problem 298, and the library writes the deduction out on its bounded-gap page. The site's curator, Thomas Bloom, is the theorem's author, so the site's label, DISPROVED (LEAN), is recorded here as the catalog's label and not as independent review.

Formalization. The linked Lean 3 declaration, pinned to its commit, is Bloom and Bhavik Mehta's own formalization of the density theorem and does not state the sequence form. The reduction from sequences to density is formalized in Lean 4 in the file src/latest/ErdosProblems/Erdos299.lean of Boris Alexeev's lean-proofs collection, linked at its pinned commit: the file declares itself a formalization of Bloom's solution, names Bloom as informal author and Mehta and Bloom as formal authors, and its not_erdos_299 shows that a strictly increasing sequence with gaps at most $C$ has upper density at least $1/(a_0+C+1)$ and applies the Lean 4 port of the density theorem, recording the axioms propext, Classical.choice and Quot.sound. A vendored copy in Jayyhk/erdos-lean, also linked, restates the result in the formal-conjectures form. The formal-conjectures file for the problem states the sequence form with a sorry body and tags the Bloom–Mehta development as the external proof. This corpus has built none of these, so the claim carries no formalized evidence.