Chess-like games and Lean?

Stream: general

[Ilmārs Cīrulis]

First, this post in thread of Combinatorial game theory repository:

Vlad Tsyrklevich said:

I ran across https://github.com/dwrensha/Chess.lean for chess a while ago but haven't really looked at it much. I think there are a couple of cool things that could be done for chess: building a theory that is useful for proving things about game play would require an algorithm for move generation which would allow proving things about chess algorithms, e.g. that an optimized bitboard move generator is correct by equivalence

Also, there's this wonderful wiki website: https://www.chessprogramming.org

Anyway, just making this thread for discussion. :)

[Violeta Hernández]

What makes a game "chess-like"? How do we distinguish between the scope of this hypothetical repository and the existing CGT repository?

[Violeta Hernández]

I do agree that there are (unfortunately) some classes of games that Conway's game theory isn't well-equipped to analyze. But what's the precise line to be drawn here?

[Ilmārs Cīrulis]

My attempt to formulate what makes game chess-like (necessary, but probably not sufficient conditions)

1) Chess game has two players, which has different possible moves in position... (Chess is partisan/partial game, if i got the terminology right.)
2) There're three possible outcomes to game (win by white, draw/tie, win by black). (No normal play convention.)
3) Chess position remains as single entity during the game, afaict.
4) Chess position becomes more simple slowly (because captures happen), and chess has endgames that can be analysed completely as shown by endgame tablebases for all 7-or-less piece endgames.

[Ilmārs Cīrulis]

Probably the title chosen by me for this thread is not good. :sweat_smile:
Changed it from "Mathematical theory of chess-like games?" to "Chess-like games and Lean?"

[Niels Feld]

If the "draw" outcome is problematic from a mathematical point of view, they are several ways to remove it from chess.
For instance, in the "Top Chess Engine Championship", they use r-mobility as a tie-break:

https://wiki.chessdom.org/R-Mobility