Erdős problem 1199

Is it true that in any 2-colouring of $\mathbb{N}$ there exists an infinite set $A$ such that all elements of $A+A$ are the same colour?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1199.lean

Retained formal statement2 of 2

Hindman [Hi79] has shown that this is false for 3-colourings.

FormalConjectures/ErdosProblems/1199.leanErdos1199.erdos_1199.variants.three1 lineExact file

1∃ color, ∀ (A : Set ℕ), A.Infinite → ∃ n ∈ A + A, ∃ m ∈ A + A, color n ≠ color m

SolvedStatement only, no proof