231.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 231

References:

erdosproblems.com/231
[Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300.
[Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
[Ke92] Keränen, Veikko, Abelian squares are avoidable on $4$ letters. Automata, languages and programming (Vienna, 1992) (1992), 41-52.
[FiPu23] Fici, Gabriele and Puzynina, Svetlana, Abelian combinatorics on words: a survey. Comput. Sci. Rev. (2023), Paper No. 100532, 21.

Imports (1)

FormalConjecturesUtil

def Erdos231.ContainsAbelianSquare A string S contains an abelian square if it has two consecutive nonempty blocks x and y such that y is a permutation of x line 40 source
Source documentation
A string S contains an abelian square if it has two consecutive nonempty blocks x and y such that y is a permutation of x.
```
def ContainsAbelianSquare {α : Type*} (S : List α) : Prop :=
…
```
theorem Erdos231.containsAbelianSquare_iff S contains an abelian square iff two consecutive blocks of some positive length L of S are permutations of each other line 46 source
Source documentation
S contains an abelian square iff two consecutive blocks of some positive length L of S are permutations of each other.
```
theorem containsAbelianSquare_iff {α : Type*} (S : List α) :
    ContainsAbelianSquare S ↔ ∃ i < S.length, ∃ L < S.length, 0 < L ∧ i + 2 * L ≤ S.length ∧
      ((S.drop i).take L).Perm ((S.drop (i + L)).take L) := by
…
```
Mentions: Erdos231.ContainsAbelianSquare
instance Erdos231.(instance at line 75) line 75 source
theorem Erdos231.not_containsAbelianSquare_example The string $1213121412132124$ of length $2^4$ over four characters contains no abelian square line 81 source
Source documentation
The string $1213121412132124$ of length $2^4$ over four characters contains no abelian square.
```
theorem not_containsAbelianSquare_example :
    ¬ ContainsAbelianSquare ([0, 1, 0, 2, 0, 1, 0, 3, 0, 1, 0, 2, 1, 0, 1, 3] : List (Fin 4)) := by
…
```
Mentions: Erdos231.ContainsAbelianSquare
theorem Erdos231.containsAbelianSquare_of_length_four Every string of length $4$ over two characters contains an abelian square line 87 source
Source documentation
Every string of length $4$ over two characters contains an abelian square.
```
theorem containsAbelianSquare_of_length_four (f : Fin 4 → Fin 2) :
    ContainsAbelianSquare (List.ofFn f) := by
…
```
Mentions: Erdos231.ContainsAbelianSquare
theorem Erdos231.containsAbelianSquare_of_length_eight Every string of length $8$ over three characters contains an abelian square line 95 source
Source documentation
Every string of length $8$ over three characters contains an abelian square.
```
theorem containsAbelianSquare_of_length_eight (f : Fin 8 → Fin 3) :
    ContainsAbelianSquare (List.ofFn f) := by
…
```
Mentions: Erdos231.ContainsAbelianSquare
theorem Erdos231.erdos_231 sorry line 121 source
theorem Erdos231.erdos_231.variants.two_pow Perhaps Erdős meant line 132 source
Source documentation
Perhaps Erdős meant $2^k$, where indeed there is an example for $k=4$: $$1213121412132124.$$ Every string of length $2^k$ over $k$ characters contains an abelian square for $k = 2, 3$, but not for $k \geq 4$.
```
theorem erdos_231.variants.two_pow : answer(False) ↔
    ∀ k : ℕ, 2 ≤ k → ∀ S : List (Fin k), S.length = 2 ^ k → ContainsAbelianSquare S := by
…
```
Mentions: Erdos231.ContainsAbelianSquare
theorem Erdos231.erdos_231.variants.two_pow_small Every string of length $2^k$ over $k$ characters contains an abelian square for $k = 2, 3$ line 141 source
Source documentation
Every string of length $2^k$ over $k$ characters contains an abelian square for $k = 2, 3$.
```
theorem erdos_231.variants.two_pow_small (k : ℕ) (hk : k = 2 ∨ k = 3) (S : List (Fin k))
    (hS : S.length = 2 ^ k) : ContainsAbelianSquare S := by
…
```
Mentions: Erdos231.ContainsAbelianSquare