Automatic proofs in combinatorial game theory

In this talk, we consider Wythoff’s game and many variations studied by Fraenkel and others. In particular, we present Walnut, a software commonly used in combinatorics on words, and show how to use it to obtain short automatic proofs of several results from the literature. We also prove a conjecture stated by Duchêne et al. regarding additional moves not changing the set of the P-positions of Wythoff’s game. We further state some new conjectures related to redundant moves. This work is linked with non-standard numeration systems for which addition is recognizable by a finite automaton. The talk is based on joint work with Bastien Mignoty, Michel Rigo and Markus Whiteland.