alt.hn

7/11/2026 at 10:11:24 PM

Combinatorial Games in Lean

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

by wertyk

7/15/2026 at 9:50:34 AM

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.

by unprovable

7/15/2026 at 10:04:28 AM

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

by wertyk

7/15/2026 at 12:50:55 PM

> 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?

by thaumasiotes

7/15/2026 at 6:30:11 PM

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.

by orangea