Problem 966

../

claims/: The 1 claim page of Problem 966, one per claimant's result; the problem's standing derives from them.

---

Statement. Let $k,r\geq 2$. Does there exist a set $A\subseteq \mathbb{N}$ that contains no non-trivial arithmetic progression of length $k+1$, yet in any $r$-colouring of $A$ there must exist a monochromatic non-trivial arithmetic progression of length $k$?

Formulation. The site's wording (the page shows no last-edited date). A non-trivial arithmetic progression has nonzero common difference. Erdős's 1975 wording (printed p. 306, quoted below) asks for "a sequence without the property $A(k+1)$, but is such that if we split it into $r$ subsequences at least one of them has the property $A(k)$", where "A sequence of integers is said to have the property $A(k)$ if it contains an arithmetic progression of $k$ terms" (p. 295); a sequence and its $r$ subsequences are the site's set and $r$-coloring. The site adds $k,r\ge2$; for $k=1$ or $r=1$ the question is trivial. Spencer's paper, the status-defining source, calls a set of integers a $V$-set (for $k$, $c$) if every $c$-coloring of it yields a monochromatic arithmetic progression of $k$ elements, and constructs such a set with no progression of length $k+1$; his $c$ is the site's $r$, his progressions have nonzero difference in both clauses, and his set is a finite subset of $\{0,\dots,p^n-1\}$ that a translation by $1$ moves into the positive integers, so the reading of $\mathbb N$ is immaterial.

Status. Proved. Spencer's Theorem 1 [Sp75] (J. Combin. Theory Ser. A 19 (1975), no. 3, 278--286; refereed) gives, for all $k$ and $c$, a $V$-set with no arithmetic progression of length $k+1$, which is the statement with $c=r$. Erdős announced the result in 1975 as "added in proof: Spencer has recently shown that such a sequence exists", without a reference; Spencer's paper is the published proof, from the Hales--Jewett theorem. The site's Lean suffix is a catalog label explained under Formalization: an external Lean proof, generated by Aristotle from the statement and posted to the site's thread by JoshuaB on 25 February 2026, exists in a later repository copy and was not built here. The claim page Spencer 1975 (accepted on the refereed publication and the curator's credit) records the result, its postings, the Aristotle-generated Lean proof behind the site's suffix and the acceptance evidence, and the frontmatter standing derives from it.

Source. erdosproblems.com/966, accessed 2026-09-18: the problem page (PROVED (LEAN), the site's label for an affirmative answer whose proof is verified in Lean; no last-edited date; source key [Er75b]), its three-comment discussion thread (25 and 26 February 2026) and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #966, https://www.erdosproblems.com/966, accessed 2026-09-18.

References.

• [Sp75] Spencer, J., Restricted Ramsey configurations. J. Combinatorial Theory Ser. A 19 (1975), no. 3, 278--286, doi:10.1016/0097-3165(75)90053-9 (the publisher's record, dates the issue November 1975). Theorem 1, printed p. 279. Library home: spencer_1975_restricted_ramsey_configurations.
• [Er75b] Erdős, P., Problems and results in combinatorial number theory. Journées Arithmétiques de Bordeaux (Conf., Univ. Bordeaux, Bordeaux, 1974), Astérisque 24--25 (1975), 295--310; Chapter IV item (i), printed p. 306, and the notation on p. 295. Library home: erdos_1975_problems_results_combinatorial_number_theory.
• [HJ63] Hales, A. W. and Jewett, R. I., Regularity and positional games. Trans. Amer. Math. Soc. 106 (1963), 222--229. Spencer's reference [5], the input of his proof; not held and not requested. Mathlib carries the theorem as Combinatorics.Line.exists_mono_in_high_dimension, which the external Lean proof below invokes.

Formalization. The site's Lean suffix is a catalog label; see "Formalization and the Lean label" below. The file ErdosProblems/966.lean of formal-conjectures at the commit linked (the head of main on 2026-09-18) declares erdos_966 : answer(True) ↔ ∀ k r : ℕ, 2 ≤ k → 2 ≤ r → ∃ A : Set ℕ, A.IsAPOfLengthFree (k + 1) ∧ ∀ coloring : A → Fin r, ContainsMonoAPofLength coloring k under category research solved, with proof sorry and a formal_proof attribute naming src/v4.29.1/ErdosProblems/Erdos966.lean in plby/lean-proofs on that repository's main branch, not a fixed commit; its docstring quotes Erdős's "Spencer has recently shown that such a sequence exists". The community database lists "proved (Lean)" and formal_status Lean as of their last update, of 25 February 2026, the statement formalized as of its last update, of 4 August 2026, and no formal-proof URL; the site's indicator reports a formalized statement. Nothing was built or kernel-checked here.

Current assessment

The question (site formulation of 2026-09-18). The statement above; PROVED (LEAN), the site's label for an affirmative answer whose proof is verified in Lean; no last-edited date. The commentary says that Erdős [Er75b] reported Spencer's result, in the words "Spencer has recently shown that such a sequence exists" (Erdős's, p. 306, quoted again below), without giving a reference, and calls the problem the arithmetic analog of the graph question, Problem 924. The thread, oldest first: a comment of 25 February 2026 by JoshuaB reporting that Aristotle produced a Lean proof of the statement in one attempt, from the statement alone and an instruction to prove it in the positive, that the commenter removed unused lemmas and fixed warnings, and that the proof builds a hypercube with the needed properties by Hales--Jewett and projects it to a lower dimension, with a link to the proof in a Lean web playground; a one-word comment of congratulation the same day; and a comment of 26 February 2026 (Terence Tao) observing that this is plausibly Spencer's own solution: the infinite cube $[k]^\omega$ has no arithmetic progression of length $k+1$, the Hales--Jewett theorem gives every finite coloring of the cube a monochromatic line, which is a $k$-term progression, and an embedding in base $q$ for any $q>2k$ (a standard Freiman-isomorphism device) projects the example onto the integers; since Mathlib has the Hales--Jewett theorem, the comment adds, the formal proof is comparatively straightforward. The proof-claim tab is empty. The community database records "proved (Lean)".

The origin (Er75b, printed p. 306). Chapter IV, item (i): "Is it true that for every $k$ and $r$ there is a sequence without the property $A(k+1)$, but is such that if we split it into $r$ subsequences at least one of them has the property $A(k)$? (added in proof: Spencer has recently shown that such a sequence exists)." The next paragraph: "The conjecture was motivated by the following older conjecture of Hajnal and myself", the graph question that is Problem 924, with Folkman's two-color theorem and the Nešetřil--Rödl theorem reported there. Property $A(k)$ is defined on p. 295. The announcement names no paper; the page below identifies it.

Status-defining source (refereed). Spencer's Theorem 1 (restricted Van der Waerden configuration; printed p. 279, checked clause by clause): "For all $k$, $c$ there exists a $V$-set $A$ such that $A$ contains no arithmetic progression of length $k+1$", where a $V$-set is a set of integers any $c$-coloring of which "yields a m.a.p. [monochromatic arithmetic progression] of size $k$". Section 2 introduces it as "a result on Van der Waerden's theorem analogous to the result of Nešetřil and Rödl", the graph theorem of Problem 924. The proof (p. 279, half a page, read for its structure): by the Hales--Jewett theorem there is $n$ such that every $c$-coloring of the cube $k^n$ has a monochromatic line; with a prime $p>k$ let $A=\{a_0+a_1p+\dots+a_{n-1}p^{n-1}:0\le a_i<k\}$; a monochromatic line of the cube is, in $A$, a monochromatic arithmetic progression of length $k$; and a progression $x,x+d,\dots,x+kd$ in $A$ is impossible because the $p^i$ digit of $x+sd$, for $d_i$ the lowest nonzero digit of $d$, runs through $k+1$ distinct residues modulo $p$ while $A$'s digits take only $k$ values. Theorem 6 (p. 285) refines the construction with $p>2k$ so that any two $k$-term progressions in the set meet in at most one point, which is the base-$q$ embedding with $q>2k$ of the thread's sketch. Acceptance: the paper appeared in J. Combinatorial Theory Ser. A 19 (1975), no. 3, 278--286 (the publisher's record), a refereed journal; Erdős's added-in-proof note attests the result, and Spencer's acknowledgment thanks Erdős "for his conjectures, theorems, and encouragement". The Semantic Scholar list of works citing the paper (28 records, 1979 to 2026, among them the restricted and canonical versions of van der Waerden's and Hales--Jewett's theorems of the 1980s and Ramsey Theory on the Integers) records no dispute. Read depth: claims checked for the definitions and Theorem 1; the proof was read for structure and not checked step by step; nothing is independently reviewed.

Formalization and the Lean label. The site's Lean suffix is a catalog label: the community database lists "proved (Lean)" as of its last update, of 25 February 2026. On that day JoshuaB posted to the thread a Lean proof that Aristotle (Harmonic) generated, as a Lean web playground page. The formal-conjectures file at the pinned commit is a statement with a sorry body whose formal_proof attribute names src/v4.29.1/ErdosProblems/Erdos966.lean in plby/lean-proofs on its main branch, a later repository copy of that proof. That repository's head on 2026-09-18 (committer date 2026-09-15) is the commit linked from the Spencer 1975 claim page; the file there (17,301 bytes; toolchain and Mathlib v4.29.1 per its header) names Spencer and Aristotle as the informal authors and Aristotle and JoshuaB as the formal authors, carries Aristotle's generation notice, defines HasAP A k ($\exists a,d$, $d\ne0$, $a+id\in A$ for $i<k$) and HasMonochromaticAP A k c for a coloring c : ℕ → Fin r, maps the cube Fin n → Fin k to $\mathbb N$ by hj_map (base $2k$), proves hj_set_no_AP and the theorem existence_of_AP_free_Ramsey_set : ∀ k r : ℕ, k ≥ 2 → r ≥ 2 → ∃ A : Set ℕ, ¬ HasAP A (k + 1) ∧ ∀ c : ℕ → Fin r, HasMonochromaticAP A k c from Mathlib's Hales--Jewett theorem; it contains no sorry and no axiom declaration, and its closing comment records #print axioms as propext, Classical.choice and Quot.sound. Its definitions differ from the collection's IsAPOfLengthFree and ContainsMonoAPofLength (which color $A$ rather than $\mathbb N$), and no bridging statement or statement-fidelity review exists here. Nothing was built or kernel-checked. The community database lists formal_status Lean as of its last update, of 25 February 2026, and no formal-proof URL.

Neighbor. Problem 924 is the graph question that motivated this one; Spencer's paper presents Theorem 1 as its arithmetic analog and, in its introduction, attests the Nešetřil--Rödl theorem that settles it.

Search scope. None of the routes below found a dispute of Spencer's theorem or a second published proof.

• The site: problem page, discussion thread and proof-claim tab; the formal-conjectures file at the pinned commit; the community database; the external Lean file at the pinned head.
• Publisher record: Crossref for [Sp75] (volume 19, issue 3, pages 278--286, November 1975).
• Semantic Scholar: the citation list of [Sp75] (28 records), scanned by title.
• arXiv: the API query abs:"restricted van der Waerden" OR abs:"restricted Ramsey" (one record, on the nilpotent polynomial Hales--Jewett theorem, which cites Spencer). The API searches titles and abstracts only.
• The primary sources: [Sp75] pp. 278--286 (Theorem 1 and its proof clause by clause; the rest as statements); [Er75b] pp. 295 and 306.

Not searched: MathSciNet, zbMATH, Google Scholar, X. Not held: [HJ63].

Remaining gaps. (1) Spencer's proof is compiled as a statement with a structural pointer; no step is independently checked. (2) The status rests on a refereed paper whose publisher's text was not compared. (3) The Lean proof behind the site's suffix was generated by Aristotle; its later repository copy was not built, and its definitions were not bridged to the collection's. (4) The site attributes the result to Spencer through Erdős's announcement alone; the identification of the paper is this page's. The label PROVED (LEAN) rests on a refereed paper and a Lean proof that was not built.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

• erdos_1975_problems_results_combinatorial_number_theory
• spencer_1975_restricted_ramsey_configurations
• spencer_1975_restricted_ramsey_configurations / theorem_1