# Which automated theorem provers can address the combinatorics of periods in strings?

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 period of $w$ if $w_i = w_{i+p},$ for all $1 \leqslant i \leqslant |w|-p.$

My questions are:

1. Which automated theorem provers are capable of formulating Theorem 1 with its proper semantics (i.e arbitrary finite strings over an arbitrary finite alphabet)?
2. 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?
3. 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?
• What does $\mathcal{P}(w') \Rightarrow \mathcal{P}(w)$ mean? – Andrej Bauer Feb 18 '14 at 7:48
• It would be helpful if you outlined the sort of proof you want automated, or at least tell us what techniques it uses. – Andrej Bauer Feb 18 '14 at 7:49
• How automated would you expect things to be. I could imagine that most common proof assistantants should be able to formulate and proove this thing, with the help of an experienced user and taking the paper you referenced as a guideline. In the end you will obtain a formal proof which can be verified automatically. If you want the proof generation to be automatic, and follow the direction of that paper, that would likely be a completely different thing. – MvG Feb 18 '14 at 8:37
• Is it just me, or is this Theorem rather trivial? You compute the length $n=\lvert w\rvert$ and period $p=\mathcal P(w)$ of $w$, then take a single one followed by $p-1$ zeros, and repeat that until the length of the word $w'$ formed in this way equals $n$. Am I missing something? – MvG Feb 18 '14 at 8:40
• @MvG: consider the word $w=001200$, with $\mathcal{P}(w)=\{4,5\}$. Note that for finite strings, the gcd of two periods need not be a period. – Neil Strickland Feb 18 '14 at 8:53

• I had a quick look at the paper of Halava et al, which is five pages long and is written explicitly as an algorithm to find $w'$. I think that anyone who was reasonably fluent with a proof assistant could encode and verify that proof without much trouble. One would expect the formalised proof to be several times longer than the paper. For this kind of work, I don't think there is much reason to prefer any one of the standard systems over the others.