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 be an infinite sequence such that is a positive unit vector (i.e. is of the form ). For which must contain a three-term arithmetic progression?
Status. SOLVED (LEAN), the site's label: the walk must contain a three-term progression exactly when . The accepted claim is Keränen's four-letter word without abelian squares, which gives the counterexamples for , together with the finite check that every ternary word of length 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 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.