Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 245

claims/: The 1 claim page of Problem 245, one per claimant's result; the problem's standing derives from them.

Statement. 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}\geq 3?

Status. Proved, the site's label: the answer is yes, by the theorem of Freĭman's 1973 monograph [Fr73], recorded on its claim page with the site's acceptance as its only evidence. The label carries no Lean qualification; a Lean development in Boris Alexeev's lean-proofs repository that declares itself a formalization of Freĭman's solution is linked from the claim page and has not been built or audited by this corpus.

Source. erdosproblems.com/245, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #245, https://www.erdosproblems.com/245.

References.

[Fr73] Freĭman, G. A., Foundations of a structural theory of set addition. (1973), vii+108.
[Ma60] Mann, H. B., A refinement of the fundamental theorem on the density of the sum of two sets of integers. Pacific J. Math. 10 (1960), 909-915.

Formalization. The statement file ErdosProblems/245.lean of formal-conjectures, at its commit of 2026-09-18, declares erdos_245 under category research solved, with the weaker bound $2$ as the variant erdos_245.variants.two, and carries no formal_proof attribute. The Lean development in Boris Alexeev's lean-proofs repository that declares itself a formalization of Freĭman's solution, with Codex and GPT-5.6 Sol as its formal authors, is linked and described on the claim page. This corpus has built and audited neither file, and no kernel credit is claimed.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (8)

Freiman's limsup bound of three for sparse sumsets problems/additive_combinatorics/E0245/claims Problem 899 Ruzsa's unbounded difference-set ratio for sparse sets Sumsets and Arithmetic Progressions A refinement of the fundamental theorem on the density of the sum of two sets of integers Theorem 2a (pp. 912-913): Theorem 2 for sets with arbitrary least elements a_0, b_0 Theorem 3 (p. 913): if (A(m)+B(m))/m has lower limit 0, then C(m) >= A(m - b_0) + B(m - a_0) - 1 for infinitely many m

Graph