---

Claim. Let the positive integers be partitioned into finitely many cells $A_1,\ldots,A_a$. Then some cell $A_i$ contains the whole finite-sums set $FS(\langle x_m\rangle_{m=1}^\infty)$ of some sequence, the set of all sums $\sum_{n\in F}x_n$ over nonempty finite $F$; this is Theorem 3.1 of Hindman (p. 9), with the notation of his Definition 2.1 (p. 1). With $a=2$ it is the statement of Problem 532: Hindman's Lemma 2.2 (p. 2) replaces the sequence by a strictly increasing one whose finite sums lie among the original ones, so its terms form the infinite set $A$ the problem asks for, and every nonempty finite subset sum of $A$ lies in the one color class $A_i$. The paper's abstract states the two-class case in words. The proof (pp. 2--9) runs through a chain of lemmas on finite-sums sets to a bounded finite form, Lemma 2.12, from which the theorem follows by compactness. Baumgartner's two-page proof of the same theorem is recorded on its own claim page.

Acceptance. Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED (LEAN) and credits Hindman with the proof, whatever the number of colors, in the problem's commentary. Refereed: N. Hindman, Finite sums from sequences within cells of a partition of $N$, J. Combin. Theory Ser. A 17 (1974), no. 1, 1--11, received 1 October 1972 and published July 1974 (Crossref record accessed). The record gives no day, so the day in the page name is a placeholder for July 1974. Erdős's surveys of 1975, 1977 and 1980 report the theorem as proved and name Baumgartner's simplification, and the 1977 and 1980 surveys add Glazer's ultrafilter proof.

Formalization. The theorem is in Mathlib: the file Mathlib/Combinatorics/Hindman.lean (linked above at a pinned commit; author David Wärn) proves it for an arbitrary additive semigroup through idempotent ultrafilters, Glazer's route, as Hindman.exists_FS_of_finite_cover and Hindman.FS_partition_regular. The file Erdos532.lean of Boris Alexeev's plby/lean-proofs collection (linked above at a pinned commit, for Lean and Mathlib v4.29.1) declares itself a formalization of Hindman's result, naming Hindman as informal author and Wärn as formal author, and derives the two-coloring statement of Problem 532 as the collection's erdos_532 states it from Mathlib's theorem, passing to a strictly increasing sequence of block sums whose finite subset sums lie in the finite-sums set of the original stream; it contains no sorry and no axiom declaration, and its closing comment records the axioms propext, Classical.choice and Quot.sound. Neither file was built here, no statement-fidelity review exists, and the convention that Lean's ℕ contains 0 while the site's $\mathbb{N}$ is the positive integers was not bridged formally, so neither is evidence listed above.

Read depth. Theorem 3.1, Definition 2.1, Lemma 2.2 and Lemma 2.12 were checked; the proof of Theorem 3.1 was followed to Lemma 2.12, and Lemmas 2.5--2.11 were read for structure only. Lemma 2.2 is proved in Hindman's 1972 paper, which was not read. Nothing here is independent review.

Depends on. Nothing in this wiki; the result is the paper's own theorem.