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

Question

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?

Answer 1

I think that

• Any of the standard theorem provers could formulate your statement without much trouble. There would be various choices about what kind of data structures to use (implicitly or explicitly), and the right choice might make a big difference to the ease of writing proofs.
• 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.
• I do not think that any existing proof assistant has any chance of finding such a proof for itself, unless you can cast the problem into a form that can be attacked by a SAT solver. I don't really know anything about SAT solvers myself but this post by Gowers seems relevant and interesting.
• If you need to enumerate a bunch of cases to consider, I would be more inclined to use a system like Maple or Mathematica (or a general programming language) to do the initial enumeration. Later on, you could feed the results into a proof assistant to validate the overall logic if necessary.