Using automata to prove theorems about sequences

Abstract: 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.

formal languages and automata theory

Audience: researchers in the topic

( paper )

One FLAT World Seminar