Automata have proven very useful in practice, both for text searching and the analysis of various kinds of discrete systems. In this talk, however, I will show that they are also useful for (rigorously) proving theorems about sequences, and hence become a new and exciting tool for number theorists and combinatorialists. As an example, I will talk about a sequence of Benoit Cloitre, defined by a certain recurrence involving Fibonacci numbers. Many properties of this sequence were conjectured, and using automata we can now resolve all of them. The proofs are done using Walnut, a free open-source theorem-prover for automatic sequences, originally designed by Hamoon Mousavi.
This is joint work with Benoit Cloitre and the paper is at https://arxiv.org/abs/2312.11706.