Automatic Theorem-Proving in Combinatorics on Words

TL;DR

This paper introduces an automated method using automata to prove theorems in combinatorics on words, demonstrated by solving an open problem related to the Thue-Morse sequence.

Contribution

It presents a novel automated technique for proving combinatorial theorems in words using automata, enabling mechanical solutions to open problems.

Findings

Successfully proved an open problem on unbordered factors in the Thue-Morse sequence

Demonstrated the effectiveness of automata-based methods in combinatorics on words

Provided a new tool for mechanical theorem proving in combinatorics

Abstract

We describe a technique for mechanically proving certain kinds of theorems in combinatorics on words, using automata and a package for manipulating them. We illustrate our technique by solving, purely mechanically, an open problem of Currie and Saari on the lengths of unbordered factors in the Thue-Morse sequence.