---

Claim. An infinite sequence $a_1,a_2,\ldots$ in $\mathbb{R}^d$ whose consecutive differences are positive unit vectors must contain a three-term arithmetic progression when $d\le 3$, and need not when $d\ge 4$. The answer to the question is therefore: exactly the dimensions $d\le 3$.

Write the walk as an infinite word over the alphabet of the $d$ unit vectors, letter $n$ recording the step $a_{n+1}-a_n$. For $i<j<k$ the vector $a_j-a_i$ counts the letters of the block of steps from position $i$ to $j$, so $a_j-a_i=a_k-a_j$ holds exactly when the two consecutive blocks of steps have the same letter counts, which forces $j-i=k-j$: a three-term progression in the walk is the same thing as an abelian square (two consecutive blocks, one a rearrangement of the other) in the word. [Ke92] constructs an infinite word over four letters with no abelian square, the fixed point of an $85$-uniform morphism, so for $d\ge 4$ a walk using four of the unit vectors has no three-term progression. For $d\le 3$, every word of length $8$ over three letters contains an abelian square (the longest abelian-square-free ternary words, such as $abacaba$, have length $7$), so every such walk contains a progression among its first nine points; this half is the classical finite check that the Fici–Puzynina survey records, not a result of [Ke92]. The site's commentary states the finite check with length $7$ in place of $8$, which $abacaba$ refutes; the discrepancy is recorded on this page and the bound $8$ is the correct one.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem solved, states the same answer and credits the $d=4$ construction to [Ke92]; and the survey of Fici and Puzynina (Comput. Sci. Rev. 2023, Theorem 16, on the library card) records four letters as the smallest alphabet on which abelian squares are avoidable, which is both halves of this claim. The paper, Keränen, V., Abelian squares are avoidable on 4 letters, in Automata, Languages and Programming (19th International Colloquium, Vienna, 13–17 July 1992), Lecture Notes in Computer Science 623, Springer (1992), 41–52, is a proceedings paper; no evidence that the volume was refereed is recorded, so refereed is not listed. The page is named by the colloquium's opening day, since the proceedings carry only the year. The site's label SOLVED (LEAN) carries a Lean mark that follows Luccioli's posts of 2026-05-09 in the site's discussion thread, which the community database records as the Lean status from 2026-05-14: a formalization of this result written with Aristotle, first in his repository KE92ErdosProblems and on 2026-05-10 as a self-contained file, whose final theorem erdos_problem_192_classification states the classification for words and checks the finite obligations of Keränen's morphism with native_decide. The catalog statement Erdos192.erdos_192, marked solved with a formal_proof link added on 2026-09-20, points at Alexeev's later Erdos192.lean of 2026-08-26 in his lean-proofs repository, which adapts Luccioli's construction and states the classification for real walks as erdos_192. Both files declare themselves formalizations of this result and are linked above; neither was built or audited by this corpus, so formalized is not listed. The acceptance rests on the curator's credit and the survey.

Depends on. No wiki page; the claim rests on the cited paper and the finite ternary check stated above.