Problem 899

Let $A\subseteq \mathbb{N}$ be an infinite set such that $\lvert A\cap \{1,\ldots,N\}\rvert=o(N)$ . Is it true that

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

Source: erdosproblems.com/899

Additive combinatorics

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

The site labels the problem PROVED (LEAN): the answer is yes. The accepted claim is Ruzsa's 1978 theorem, which the site credits with the proof, recorded on its claim page (Ruzsa, 1978) with the curator's acceptance as its evidence; the label's Lean mark refers to a Lean development of 2026 in Boris Alexeev's lean-proofs repository that declares itself a formalization of Ruzsa's proof, linked on the claim page; that file is not among the Lean the corpus has built and audited, so no formalized evidence is listed. The sumset analogue is Problem 245.

Problem 899

Status

Proof claims

Discussion