---

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

$$\limsup_{N \to \infty} \frac{\lvert (A+A) \cap \{1, \ldots, N\} \rvert} {\lvert A \cap \{1, \ldots, N\} \rvert} \geq 3,$$

which answers Problem 245 yes. The constant $3$ is best possible, as Erdős noted when posing the question. The source is G. A. Freiman, Foundations of a structural theory of set addition, Translations of Mathematical Monographs 37, American Mathematical Society, Providence, 1973, vii+108 pp., translated from the 1966 Russian original. The monograph is not held in the library and no theorem number is recorded; the attribution is the site's. The page is dated to the translation's year because no publication day is recorded. The weaker bound with $2$ in place of $3$, which Erdős called easy, follows from Mann's 1960 refinement of the $\alpha + \beta$ theorem (Mann 1960); that bound is not a claim about the question as asked.

Formalization. The Lean file src/latest/ErdosProblems/Erdos245.lean of Boris Alexeev's lean-proofs repository, linked above at a pinned commit (file first published 2026-08-23), declares itself a formalization of a solution to Problem 245 and names Gregory Freiman as its informal author and Codex and GPT-5.6 Sol as its formal authors, so it is recorded on this page as a formalization of this claim rather than as an independent result. Its theorem erdos_245 asserts, for every infinite $A\subseteq\mathbb N$ with $|A\cap\{1,\ldots,N\}|/N\to0$, that the upper limit of the ratio of the sumset count to the set count up to $N$ is at least $3$. Its header says that the imported development proves the finite ingredients, a stopping-scale lemma, a diameter bound for proper generalized arithmetic progressions and the sharp $3k-4$ inverse step, before assembling the statement. The file contains no sorry and no axiom command at the pinned commit and imports a companion module of the same repository. The site's label carries no Lean qualification, and the formal-conjectures statement file does not point to this development. This corpus has not built the file or audited its statement against the problem, so no formalized evidence is listed.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem proved on erdosproblems.com and credits Freiman [Fr73] with the proof that the answer is yes; the curator's acceptance is the documented acceptance. The monograph is a published book, not a journal article, so no refereed publication is listed, and no proof is compiled in this corpus.