Variants of Wythoff game with terminal positions or blocking maneuvers

TL;DR

This paper demonstrates how the Walnut software can automatically prove and extend results on variants of the Wythoff game with added terminal positions or blocking moves, using recursive characterizations and Fibonacci-based techniques.

Contribution

It introduces a novel application of Walnut for automated proofs in combinatorial game theory and extends understanding of Wythoff game variants with new characterizations.

Findings

Walnut effectively automates proofs of Wythoff game variants.

New recursive and morphic characterizations of Wythoff-type games.

Application of Fibonacci numeration system to solve game instances.

Abstract

We show how the software Walnut can be used to obtain concise proofs of results concerning variants of the famous Wythoff game, in which blocking maneuvers or terminal positions are added, as discussed respectively by Larsson (2011) and Komak et al. (2025). Our approach provides automatic proofs that both confirm and extend their results, and the same techniques apply to newly introduced variants as well. Then, using classic techniques, we obtain new recursive and morphic characterizations of Wythoff-type games where the set of terminal positions $(x,y)$ satisfy $x+y\le\ell$. The use of Walnut in combinatorial game theory is relatively recent, and only a few examples have been explored so far. The Wythoff game, being directly connected to the Fibonacci numeration system, proves especially well-suited to this kind of approach. It permits us to solve instances for a fixed value of a parameter.