Erdős Problem 109

References:

• erdosproblems.com/109
• [MRR19] J. Moreira, F.K. Richter, and D. Robertson, A proof of a sumset conjecture of Erdős, Annals of Math. 189 (2019), 605-652.

theorem Erdos109.erdos_109 (A : Set ℕ) (h : A.upperDensity > 0) : ∃ (B : Set ℕ) (C : Set ℕ), B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

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

The Erdős sumset conjecture. Proved by Moreira, Richter, and Robertson [MRR19].