---

Claim. Spencer's Theorem 1 (J. Combinatorial Theory Ser. A 19 (1975), p. 279) states that for all $k$ and $c$ there is a $V$-set $A$ containing no arithmetic progression of length $k+1$, where a $V$-set is a set of integers every $c$-coloring of which yields a monochromatic arithmetic progression of $k$ terms. With $c=r$ this answers Problem 966 yes for every $k,r\ge2$: the set $A$ has no non-trivial progression of length $k+1$, and every $r$-coloring of it has a monochromatic non-trivial progression of length $k$. The set is $A=\{a_0+a_1p+\dots+a_{n-1}p^{n-1}:0\le a_i<k\}$ for a prime $p>k$ and $n$ the Hales--Jewett dimension for $k$ and $c$; it is finite, lies in $\{0,\dots,p^n-1\}$, and a translation by $1$ places it in the positive integers. Both clauses concern progressions with nonzero difference. The proof is half a page: a $c$-coloring of $A$ is a $c$-coloring of the cube $k^n$, whose monochromatic line, given by the Hales--Jewett theorem, is a $k$-term progression in $A$; and a progression $x,x+d,\dots,x+kd$ in $A$ is impossible, because at the position of the lowest nonzero base-$p$ digit of $d$ the digits of the terms run through $k+1$ distinct residues modulo $p$ while the digits of elements of $A$ take only $k$ values.

Scope. Full: the theorem is the problem's statement for every $k$ and $r$, the site's $k,r\ge2$ included.

Depends on. Nothing in this wiki; the result rests on the cited paper and the Hales--Jewett theorem it invokes.

Acceptance. Reviewed: the site's curator, Thomas Bloom, marks the problem PROVED (LEAN) and, in the problem's commentary, credits the result to Spencer through Erdős's announcement; the Lean proof behind the label is described under Formalization. The curator's credit rests on Erdős's note, not on a reading of Spencer's paper, which the commentary does not cite and the thread does not discuss. Refereed: the paper appeared in J. Combinatorial Theory Ser. A 19 (1975), no. 3, 278--286 (the Crossref record dates the issue November 1975 without a day, so the page's day is a placeholder). Erdős's 1975 Bordeaux paper announced the result in an added-in-proof note that gives no reference (source card); the identification of Spencer's paper as the published proof is the problem page's, and Spencer's acknowledgment thanks Erdős for his conjectures. The Semantic Scholar list of 28 citing works records no dispute.

Formalization. The Lean proof behind the site's suffix is an independent proof that Aristotle (Harmonic) generated from the statement alone and the forum user JoshuaB posted to the site's thread on 25 February 2026 (post 4472, linked above). Its repository copy, the file src/v4.29.1/ErdosProblems/Erdos966.lean in Boris Alexeev's repository plby/lean-proofs (linked above), names Spencer and Aristotle as informal authors and Aristotle and JoshuaB as formal authors, and proves the statement with colorings of $\mathbb N$ in place of colorings of $A$. Its construction is the one above with base $2k$ in place of the prime $p$. The corpus has not built or audited the file and no statement-fidelity review of it exists, so the page lists no formalized evidence.

Read depth. The definitions and Theorem 1 were checked clause by clause, and the proof for its two steps, not step by step. Nothing here is independent review.