Five years ago, I made a conjecture on the number of correlation classes that are exhibited by pairs of words in an alphabet of a given size. I later speculated that the conjecture could be tackled via automated theorem proving. I would now like to make some progress on this conjecture, by finding out whether there are any automated theorem provers capable of at least formulating a simpler statement along the same lines.

The simpler statement that I have chosen is Theorem 1 of Halava, V., Harju, T., & Ilie, L. (2000). *Periods and binary words*. Journal of Combinatorial Theory, Series A, 89(2), 298-303. This theorem is a restatement of part of Theorem 5.1 of Guibas, L. J., & Odlyzko, A. M. (1981). Periods in strings. Journal of Combinatorial Theory, Series A, 30(1), 19-42:

Theorem 1: For any alphabet $A$ and any word $w \in A^*$, there exists a word $w' \in \{0,1\}^*$ such that $\mathcal{P}(w') = \mathcal{P}(w).$

Here $\mathcal{P}(w)$ is the set of *periods* of the word $w$:

An integer $p,$ with $1 \leqslant p \leqslant |w|,$ is called a

periodof $w$ if $w_i = w_{i+p},$ for all $1 \leqslant i \leqslant |w|-p.$

My questions are:

- Which automated theorem provers are capable of formulating Theorem 1 with its proper semantics (i.e arbitrary finite strings over an arbitrary finite alphabet)?
- Which automated theorem provers are cable of
*proving*Theorem 1, along the lines of Guibas and Odlyzko, or Halava, Harju and Ilie, or in an otherwise intelligible manner? - How much work would be involved in creating such a formulation and proof? Would this be an undergraduate student assignment, a PhD project, or a decades-long project for a research team? Or would it require the development of new types of theorem provers?

generationto be automatic, and follow the direction of that paper, that would likely be a completely different thing. $\endgroup$4more comments