---

Claim. The answer to [[problems/discrete_geometry/E1090/_index|Problem 1090]] is yes for every $k\geq3$. By the Hales–Jewett theorem there is an $n$ such that every two-coloring of the cube $[k]^n$ has a monochromatic combinatorial line, a set of $k$ points obtained by letting a nonempty set of coordinates run through $1,\dots,k$ together while the rest stay fixed. Map the cube into the plane by a generic linear projection: the images of the $k$ points of a combinatorial line are collinear and equally spaced, the map is injective, and no other point of the cube lands on the line through them. The image $A$ is a finite plane set, and any two-coloring of $A$, pulled back to the cube, yields a monochromatic combinatorial line whose image is a line containing exactly $k$ points of $A$, all of one color.

Claimant. Zach Hunter posted the argument in the problem's discussion on 2025-10-17, in one sentence: recall Hales–Jewett and project $[k]^n$ generically into the plane. The site's commentary records the observation and acknowledges Hunter as a contributor. Erdős's 1975 paper (card, Section 4, p. 106), the problem's source, reports that "GRAHAM and SELFRIDGE gave an affirmative answer for $k=3$, but the cases $k>3$ seem to be open"; no publication of the $k=3$ argument is recorded, and the report is a pending partial claim on its own claim page.

Depends on. No page of this wiki.

Formalization. A Lean proof in Boris Alexeev's repository of Lean proofs of Erdős problems, linked above at a pinned commit, declares itself a formalization of this solution with Hunter as informal author and Aristotle, Gemini 3.0 Flash and the forum account JoshuaB as formal authors. JoshuaB reported it in the discussion on 2026-02-27: Aristotle (Harmonic) produced most of the proof from the formal statement and a hint naming Mathlib's Hales–Jewett theorem, its first theorem asking only that the $k$ collinear points share a color, and Gemini 3.0 Flash stated and proved the strict form in which every point of $A$ on the line has that color, the problem's condition; the file proves both and contains no sorry. The formal-conjectures statement file marks the problem solved and points to this file at its repository's main branch. This corpus has not built or audited the development, so it is a link and not evidence.

Acceptance. Thomas Bloom, the site's curator, labels the problem proved and credits Hunter's observation in the problem's commentary on the problem's page at erdosproblems.com (page last edited 2025-10-19); that credit is the reviewed evidence. There is no refereed write-up, and the Lean proof is third-party Lean, so the claim is neither refereed nor formalized.