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

Updated Oct 8

Problem 109

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

Statement. Any $A\subseteq \mathbb{N}$ of positive upper density contains a sumset $B+C$ where both $B$ and $C$ are infinite.

Status. PROVED (LEAN), the site's label; its suffix is a catalog label explained under Formalization. The status-defining source is Theorem 1.2 of Moreira, Richter and Robertson (Ann. of Math. (2) 189 (2019), 605--652, refereed), which proves the statement for positive upper density along any Følner sequence; the site's statement is the case of the intervals $\{1,\ldots,N\}$ . The claim page is Moreira, Richter and Robertson, accepted on the site curator's credit and the refereed publication; the 2026 Lean development that declares itself a formalization of their theorem is linked there and gives no formalized evidence, since this corpus has not built or audited it.

Source. erdosproblems.com/109, accessed 2026-10-07 (page last edited 27 September 2025; empty proof-claim tab). Cite as: T. F. Bloom, Erdős Problem #109, https://www.erdosproblems.com/109.

References.

[MRR19] Moreira, Joel and Richter, Florian K. and Robertson, Donald, A proof of a sumset conjecture of Erdős. Ann. of Math. (2) 189 (2019), no. 2, 605-652, doi:10.4007/annals.2019.189.2.4 (Crossref record of 2026-10-07); arXiv:1803.00498 (v1 of 1 March 2018; v6 of 13 June 2019, the edition cited here, not the journal version, which predates its correction of the proof of Theorem 3.22). Library home: moreira_2019_proof_sumset_conjecture_erdos.

Formalization. The site's label is PROVED (LEAN); its suffix is a catalog label. The statement is in formal-conjectures, with formal-conjectures' Set.upperDensity (Mathlib has no upper-density definition); at its commit of 2026-10-06, linked, the file is tagged solved and names line 9074 of src/latest/ErdosProblems/Erdos109.lean of Boris Alexeev's lean-proofs repository as the formal proof, and that file takes the definition from its own Util.Density, a modified copy of the formal-conjectures file. The community database (teorth/erdosproblems, file commit of 2026-09-28) lists status "proved (Lean)", formal_status Lean as of that field's last update on 2026-08-23, and formalized "yes" as of its last update on 2026-01-12. The development (added 2026-08-20) is pinned on the Moreira, Richter and Robertson claim page as a formalization of their theorem. This corpus has not built or checked it, and no local 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 (11)

Moreira, Richter and Robertson prove the sumset conjecture problems/additive_combinatorics/E0109/claims Kra, Moreira, Richter and Robertson prove the B + B + t conjecture Sumsets and Arithmetic Progressions additive_combinatorics/moreira_2019_proof_sumset_conjecture_erdos Theorem 1.2: a set of positive upper density along some Følner sequence contains B + C with B, C infinite Theorem 1.3: in a countable group, a set of positive upper density along a two-sided Følner sequence contains BC with B, C infinite Theorem 2.2: a positive ultrafilter limit of densities of (A - n) ∩ (A - p) gives B + C inside A Theorem 2.7: for bounded non-negative f, some ultrafilter p has lim <R^m f, R^p f> at least <1, f>^2 - epsilon Theorem 3.22: every f in L^2(N, Phi) splits along a subsequence into a compact part and a weak mixing part Theorem 3.6: every f in L^2(N, Phi) splits along a subsequence into a Besicovitch almost periodic part and a part orthogonal to all characters

Graph