Erdős Problem 949

Reference: erdosproblems.com/949

theorem Erdos949.erdos_949 : (∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Set.univ \ S, Cardinal.mk ↑A = Cardinal.continuum ∧ A + A ⊆ A) ↔ sorry

Let $S \\subseteq \\mathbb{R}$ be a set containing no solutions to $a + b = c$. Must there be a set $A \\subseteq \\mathbb{R} \\setminus S$ of cardinality continuum such that $A + A \\subseteq A$?

theorem Erdos949.erdos_949.variants.sidon : (∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Set.univ \ S, Cardinal.mk ↑A = Cardinal.continuum ∧ A + A ⊆ A) ↔ sorry

Let $S\sub \mathbb{R}$ be a Sidon set. Must there be a set $A\sub \mathbb{R}∖S$ of cardinality continuum such that $A + A \sub A$?