Automatic proofs in combinatorial game theory

We consider Wythoff’s game and many variations studied by Fraenkel and others. We show how to use automatic theorem-prover Walnut 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 Beatty sequences, (quadratic) Pisot numbers and non-standard numeration systems for which addition is recognizable by a finite automaton.