Skip to content

Erdős problem 532

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

532.lean

Retained formal statement1 of 1

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

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

FormalConjectures/ErdosProblems/532.leanErdos532.erdos_5321 lineExact file
True ↔ ∀ (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.

Search problems.science

Find a Problem, Result, source, or page