HEXAGONbeta

The minimum number of distinct abelian squares in a binary circular word

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatoricscs.DM — Discrete Mathematicscs.FL — Formal Languages and Automata Theory

Contributed by Deep Bhattacharjee ↗

Version 1 / Oct 22, 2026 / CC BY 4.0

Abstract

We prove that every binary circular word of length nn contains at least $\fl{(n-1)/2}$ distinct abelian squares, and we determine all words attaining this bound. This settles a conjecture of Simpson: its odd case holds, and in its even case the list of extremal words misses (ab)n/2(ab)^{n/2} for n≡2(mod4)n\equiv 2\pmod 4, n≥6n\ge 6.

Provenance statement

Deep Bhattacharjee chose the problem, Conjecture 0.6 of J. Simpson (arXiv:1802.04481), and directed the work. Claude (Anthropic), working through Claude Code, did the following: - searched the literature; - found and checked the proofs; - wrote the Lean 4 formalization and the verification programs; - drafted the paper. For each half-length m, the proof counts the pairs (last letter of the left half, its count) over the abelian squares of half-length m. These pairs for m and n − m are in bijection. Every pair (l, k) with 1 ≤ k < |w|_l occurs, which gives D(w) ≥ floor((n−1)/2). In the case of equality, an analysis of the runs of one letter gives the extremal words. The six main theorems are proved in Lean 4 with Mathlib, and they depend only on propext, Classical.choice and Quot.sound. Independent programs check the results: - in C, every word with n ≤ 22; - in C++, every necklace with n ≤ 28; - in Python, n ≤ 12; - in Julia, every lemma with n ≤ 16; - in Bash, n ≤ 10. Code and proofs: release v2.1.0, https://github.com/creelie/literate-octo-lamp/releases/tag/v2.1.0.
AI provenance filesAI-PROVENANCE-HEXAGON.md · 2 KB

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. J. Simpson, Solved and unsolved problems about abelian squares, preprint (2018), arXiv:1802.04481.arXiv
  2. A.\,S. Fraenkel, J. Simpson, M. Paterson, On weak circular squares in binary words, in: Combinatorial Pattern Matching (CPM 1997), Lecture Notes in Computer Science, Springer, 1997, pp. 76--82, doi:10.1007/3-540-63220-4_51 (https://doi.org/10.1007/3-540-63220-4_51).DOI
  3. S.\,Z. Fazekas, A. Mammoliti, R. Mercaş, J. Simpson, Binary words containing few abelian squares, preprint (2026), arXiv:2604.23188.arXiv
  4. G. Fici, F. Mignosi, Words with the maximum number of abelian squares, in: Combinatorics on Words (WORDS 2015), Lecture Notes in Computer Science, Springer, 2015, pp. 122--134, doi:10.1007/978-3-319-23660-5_11 (https://doi.org/10.1007/978-3-319-23660-5_11).DOI
  5. G. Fici, F. Mignosi, J. Shallit, Abelian-square-rich words, Theoret. Comput. Sci. 684 (2017) 29--42, doi:10.1016/j.tcs.2017.02.012 (https://doi.org/10.1016/j.tcs.2017.02.012).DOI
  6. G. Fici, S. Puzynina, Abelian combinatorics on words: a survey, Comput. Sci. Rev. 47 (2023) 100532, doi:10.1016/j.cosrev.2022.100532 (https://doi.org/10.1016/j.cosrev.2022.100532).DOI
  7. L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction -- CADE 28, Lecture Notes in Computer Science, Springer, 2021, pp. 625--635, doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  8. The mathlib Community, The Lean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, pp. 367--381, doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 22, 2026