Automatic proofs in combinatorial game theory

Michel Rigo (U Liege)

Apr 24. 2025, 09:30 — 10:00

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.

Further Information
Venue:
ESI Boltzmann Lecture Hall
Recordings:
Recording
Files:
Slides
Associated Event:
Uniform Distribution of Sequences (Workshop)
Organizer(s):
Henk Bruin (U of Vienna)
Robbert Fokkink (TU Delft)
Jörg Thuswaldner (Montanuniversität Leoben)