Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 192

../

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


Statement. Let A={a1,a2,…}⊂RdA=\{a_1,a_2,\ldots\}\subset \mathbb{R}^d be an infinite sequence such that ai+1−aia_{i+1}-a_i is a positive unit vector (i.e. is of the form (0,0,…,1,0,…,0)(0,0,\ldots,1,0,\ldots,0)). For which dd must AA contain a three-term arithmetic progression?

Status. SOLVED (LEAN), the site's label: the walk must contain a three-term progression exactly when d≤3d\le 3. The accepted claim is Keränen's four-letter word without abelian squares, which gives the counterexamples for d≥4d\ge 4, together with the finite check that every ternary word of length 88 contains an abelian square, recorded on its claim page with its curator and survey evidence; the label's Lean mark follows Luccioli's Lean proof of the full classification posted in the site's thread in May 2026, and the catalog links Alexeev's later file of August 2026, both listed on the claim page and not built by this corpus.

Source. erdosproblems.com/192, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #192, https://www.erdosproblems.com/192.

References.

  • [FiPu23] Fici, Gabriele and Puzynina, Svetlana, Abelian combinatorics on words: a survey. Comput. Sci. Rev. (2023), Paper No. 100532, 21.
  • [Ke92] Keränen, Veikko, Abelian squares are avoidable on 44 letters. Automata, languages and programming (Vienna, 1992) (1992), 41-52.

Formalization. Statement in formal-conjectures; the Lean proofs are listed on the claim page.

Progress

Not yet compiled.

Known Results

Not yet compiled.

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.