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

Worked, still open.

additive combinatorics · solved · formalized (Lean) · 0 attempts

machinery: additive-combinatorics,sumset-B+C-infinite,ergodic-correspondence,upper-Banach-density,Furstenberg-correspondence,formalization-gap

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 5 · solved (literature)

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

solved