Erdős problem 532

If $\mathbb{N}$ is 2-coloured then is there some infinite set $A\subseteq \mathbb{N}$ such that all finite subset sums $\sum_{n\in S}n$ (as $S$ ranges over all non-empty finite subsets of $A$ ) are monochromatic?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

532.lean

Retained formal statement1 of 1

If $\mathbb{N}$ is 2-coloured then is there some infinite set $A\subseteq \mathbb{N}$ such that all finite subset sums $\sum_{n\in S}n$ (as $S$ ranges over all non-empty finite subsets of $A$ ) are monochromatic?

Asked by Graham and Rothschild. Proved by Hindman [Hi74] (for any number of colours).

FormalConjectures/ErdosProblems/532.leanErdos532.erdos_5321 lineExact file

1True ↔ ∀ (c : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∃ color, ∀ (S : Finset ℕ), S.Nonempty → ↑S ⊆ A → c (∑ n ∈ S, n) = color

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.