4 ms·

Combinatorial Games in Lean

• unprovable 3mo 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 3mo ago
    Not the author, I just submitted the link — vihdzp maintains the repo. An issue over there would actually reach them.)
• thaumasiotes 3mo 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 3mo 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.
    • thaumasiotes 3mo 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?