Jeffrey Shallit, School of Computer Science, University of Waterloo

In this talk, I will show how to guess and prove theorems in combinatorics on words using the Walnut prover, written by Hamoon Mousavi. As an example, we recently proved the following result: the infinite word

r = 001001101101100100110110110010010011011001001001101100100100 ...

generated as the fixed point of the map a -> abcab, b -> cda, c -> cdacd, d -> abc, followed by the coding sending a, b -> 0 and c, d -> 1, is aperiodic and avoids the pattern x x x^R, where x^R denotes the reversal of x. This is the first nontrivial result on avoidance in words obtained through the use of a prover. This is joint work with Chen Fei Du, Hamoon Mousavi, Eric Rowland, and Luke Schaeffer.