---

Claim. The answer is no. Veikko Keränen proves, in Abelian squares are avoidable on 4 letters, that there is an infinite word over a four-letter alphabet in which no two consecutive blocks of equal length are permutations of each other: the fixed point of an explicit $85$-uniform substitution on four letters, which maps abelian-square-free words to abelian-square-free words. Every prefix of that word is abelian-square-free, so for every $k\geq4$ and every length, in particular length $2^k$, there is a string over $k$ characters with no abelian square, and the corrected Statement of Problem 231 has a negative answer for every $k\geq4$. This is the first part of Theorem 16 in the survey of Fici and Puzynina (card), which also records that four letters are the fewest possible, after Evdokimov's $25$ letters and Pleasants's $5$, and that the number of abelian-square-free words of length $n$ on four letters grows exponentially. The site's wording, with length $2^k-1$, fails at every $k$ without this theorem, by the doubling words $Z_k=Z_{k-1}\,k\,Z_{k-1}$, with $Z_1=1$, as the problem page's Notes record. What the theorem settles is more than the corrected Statement: no length at all forces an abelian square on four letters, so $N(4)$ is infinite in Erdős's 1957 notation, and the question Erdős asked next, whether an infinite string on four symbols can avoid abelian squares (Problem 192 on the site), is answered. Erdős's own 1957 and 1961 formulations and his report of a finite disproof at $k=4$ with de Bruijn are recorded on the de Bruijn–Erdős page.

Acceptance. Reviewed: Thomas Bloom, the site's curator, marks the problem disproved and credits the negative answer for all $k\geq4$ to Keränen [Ke92]; the survey of Fici and Puzynina, Comput. Sci. Rev. 47 (2023), states the theorem with Keränen's attribution and the optimality of the alphabet size. The paper itself appeared in the proceedings of ICALP 1992 (Lecture Notes in Comput. Sci. 623, Springer, 41–52), a conference volume rather than a journal, so the page lists no refereed evidence; the proceedings carry only the year, so the page is named by the colloquium's opening day, 13 July 1992.

Formalizations. One Lean 4 development declares itself a formalization of Keränen's theorem and of its consequence for this problem: the repository KE92ErdosProblems, published by Lorenzo Luccioli on 2026-05-09 and completed on 2026-05-10, whose solutions its README attributes to Harmonic's Aristotle. Its endpoint KE92.erdos_problem_231 states that some $f:\mathbb N\to\{0,1,2,3\}$ is abelian-square-free, and erdos_problem_231_finite derives an abelian-square-free word of every length on four letters; the bounded checks of the morphism use native_decide, as the development's own module notes say. Luccioli posted the repository on the site's discussion thread on 2026-05-09, reporting a first version whose large case analysis took hours to compile and a second with a more algebraic argument, and a self-contained file on 2026-05-10, both linked above at their pinned revisions. The community database lists the site's label with its Lean qualifier as of its last update of 2026-05-14. None of this Lean was built or audited here, so the page lists no formalized evidence.