---

Claim. Let $A\subseteq\mathbb N$ be infinite with $\lvert A\cap\{1,\ldots,N\}\rvert=o(N)$. Then

$$\limsup_{N\to\infty}\frac{\lvert(A-A)\cap\{1,\ldots,N\}\rvert} {\lvert A\cap\{1,\ldots,N\}\rvert}=\infty,$$

which answers Problem 899 yes. The source is I. Z. Ruzsa, On the cardinality of $A+A$ and $A-A$, in: Combinatorics (Keszthely, 1976), Colloquia Mathematica Societatis János Bolyai 18, North-Holland (1978), 933--938, cited as [Ru78] on the problem page, whose reference omits the venue; the volume is the proceedings of the fifth Hungarian combinatorial colloquium. No theorem number is cited; the attribution is the site's, and the page is dated to the volume's year because no publication day is recorded. The sumset analogue, with $\limsup\ge3$ in place of $\infty$, is Problem 245, which the site credits to Freiman.

Postings. Boris Alexeev's lean-proofs repository holds a Lean 4 file, added 2026-08-15 and linked above at the revision the formal-conjectures catalog pins, whose header declares it a formalization of Ruzsa's solution (Ruzsa as informal author, the systems Codex and GPT-5.6 Sol as formal authors) and whose module comment describes the argument as Ruzsa's translate-layer proof. Its final theorem erdos_899 states, for every infinite $A\subseteq\mathbb N$ whose counting function is $o(N)$, that the limsup over $N$ of the ratio of $\lvert(A-A)\cap[1,N]\rvert$ to $\lvert A\cap[1,N]\rvert$, taken in the extended reals, is $+\infty$, which is the formal-conjectures catalog's statement; its closing line prints the axioms of that theorem. The formal-conjectures catalog's statement file, whose own theorem is sorry, marks the statement solved with a formal_proof link to that file, and the site's label reads PROVED (LEAN). Neither file is among the Lean the corpus has built and audited, so no formalized is listed.

Depends on. No wiki page; the claim rests on the cited paper.

Acceptance. Reviewed: the site's curator, Thomas Bloom, marks the problem proved on erdosproblems.com and credits Ruzsa [Ru78] with the proof that the answer is yes, and the formal-conjectures catalog marks its statement solved with the formalization linked; the curator's acceptance is the documented acceptance. The paper appeared in a colloquium proceedings volume, so no refereed journal publication is listed; the Lean file is not among the Lean the corpus has built and audited, so formalized is not listed although the site's label reads PROVED (LEAN).