Combinatorial Games in Lean

Neat! Perhaps add a wishlist or Project tab? :)

Tangentially, I recall reading a paper not that long ago that showed that under certain assumptions that Zermelo's theorem showed that making the games 'quantum games' didn't actually offer any real advantage.

> A combinatorial game is two-player terminating game with perfect information. In other words, two players (called Left and Right) alternate changing some game state, which they always have full knowledge of. The game cannot go on forever, and whoever is left without a move to make loses. There are no draws.

> Non-examples include [...] Chess, which can end in a tie

And yet, somehow, tic-tac-toe is considered a combinatorial game. Not only can it end in a tie, it always will unless one player is very new to the game.

If we're willing to count tic-tac-toe by defining some tie states as victories for one side, why can't we do the same thing with chess?