Erdős problem 949
Let be a set containing no solutions to . Must there be a set of cardinality continuum such that ?
Sources
FormalConjectures/ErdosProblems/
949.lean
Retained formal statement
Let be a set containing no solutions to . Must there be a set of cardinality continuum such that ?
True ↔ ∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, Cardinal.mk ↑A = Cardinal.continuum ∧ A + A ⊆ SᶜOpenStatement only, no proof