Combinatorial Games in Lean

https://github.com/vihdzp/combinatorial-games

by wertyk • 11 days ago

40 5 11 days ago

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.

wertyk• 8 days ago

Not the author, I just submitted the link — vihdzp maintains the repo. An issue over there would actually reach them.)

thaumasiotes2• 7 days ago

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?

orangea• 7 days ago

It probably has more to do with the fact that formalizing chess in such a way wouldn't be particularly interesting. Chess is mostly studied because of its historical significance, and if you change the rules then the game no longer is as connected to its historical significance.

thaumasiotes2• 6 days ago

The page already has formalized chess that way. It states that the loser is the first player to have no legal move when their turn occurs. This definition applies to chess with no modification.

But the page also states that chess doesn't meet its definition of a combinatorial game. Why?

Combinatorial Games in Lean

Related Stories