Automatic Proofs in Combinatorial Game Theory

Explore automatic theorem-proving techniques in combinatorial game theory in this 26-minute talk by Michel Rigo at the Workshop on "Uniform Distribution of Sequences" held at the Erwin Schrödinger International Institute for Mathematics and Physics (ESI). Discover how Wythoff's game and its variations can be analyzed using the automatic theorem-prover Walnut to obtain concise proofs of established results. Learn about a proven conjecture regarding additional moves not affecting P-positions in Wythoff's game, and encounter new conjectures about redundant moves. Connect these concepts to Beatty sequences, quadratic Pisot numbers, and non-standard numeration systems where addition is recognizable by finite automata.