Combinatorial game theory repository

Stream: general

[Violeta Hernández]

Discussion thread for #announce > Combinatorial game theory repository @ 💬.

[Violeta Hernández]

It's probably worth pointing out there's some quite major changes from the Mathlib repository. Most notably, we implemented the long-awaited IGame refactor, to the extent that the previous PGame now plays only the role of an auxiliary construction.

[Kevin Buzzard]

Could you ever envisage an interface where people could actually play some of these games rather than just proving theorems about them? What would that entail? First step would be e.g. two players playing against each other, you might have to implement a way of visualising a position on a per-game basis. The reason I think this is a cool next step is that the moment you have something where people can play, you might get people organically thinking "hey wouldn't it be cool if I could write an algorithm to play for me"; my feeling is that this is more likely to happen if the GUI is already there though.

[Kevin Buzzard]

Re the README: are you sure Tic-Tac-Toe and chess are combinatorial games? I thought neither of them were played under the "normal play rule" ("you lose precisely when you can't move") and furthermore chess can go on forever unless you invoke the 50 move rule which again is not part of the normal play rule (and means that it's not true that the moves are determined by the position alone). Or is there some hack to make this true?

[Aaron Liu]

Kevin Buzzard said:

Re the README: are you sure Tic-Tac-Toe and chess are combinatorial games? I thought neither of them were played under the "normal play rule" ("you lose precisely when you can't move") and furthermore chess can go on forever unless you invoke the 50 move rule which again is not part of the normal play rule (and means that it's not true that the moves are determined by the position alone). Or is there some hack to make this true?

Hack for tic-tac-toe: if the other player has a three-in-a-row, you have no moves.

[Ilmārs Cīrulis]

About chess - if we count the repetition of position as a draw then there are no infinite games.

[Adam Topaz]

Ping @Owen Randall

[Kevin Buzzard]

Yes I kind of realised the tic-tac-toe hack as I was writing. I can't really make it work for chess though. I think that in theory a game can go on forever? Don't the players actually have to agree on a draw after 50 moves, rather than it being forced on them?

[Aaron Liu]

Ilmārs Cīrulis said:

About chess - if we count the repetition of position as a draw then there are no infinite games.

What is a "draw"?

[Aaron Liu]

Kevin Buzzard said:

Yes I kind of realised the tic-tac-toe hack as I was writing. I can't really make it work for chess though. I think that in theory a game can go on forever? Don't the players actually have to agree on a draw after 50 moves, rather than it being forced on them?

According to my hazy memory, after 75 moves the proctor declares a draw, with no input from the players.

[Kevin Buzzard]

What is a "draw"?

Aah good point, that's not really a thing in CGT right? (unless you're asking a UK/US English question, in which case the answer is "a tie" :-))

[Ilmārs Cīrulis]

https://en.wikipedia.org/wiki/Fifty-move_rule#Seventy-five-move_rule - yup

[Ilmārs Cīrulis]

Lechenicher SchachServer enforces 50 move automatically. It also stops game when 7-piece position is reached and adjudicates automatically by consulting endgame tablebases. ICCF does the same, afaik. (I don't play on it.)

FICGS, I believe, simply ignores 50 move rule.

[Ilmārs Cīrulis]

So, there are many "different" chess types around here. :sweat_smile:

[Owen Randall]

Yeah I don’t think you could consider Tic Tac Toe or chess as normal play games due to drawing and stalemates, even with the no moves on loss hack. You would have to declare one player a winner of the tie (i.e. Go uses non-integer Komi values for tie breaking) but at that point it’s a different game with new properties. As they aren’t normal play I doubt you could apply much CGT theory to these games.

[Violeta Hernández]

Kevin Buzzard said:

Could you ever envisage an interface where people could actually play some of these games rather than just proving theorems about them? What would that entail?

I don't see why something like this couldn't be implemented. "Concrete" games like e.g. domineering are first implemented as the type of all their states, and turning them into our game structure IGame requires providing the well-founded relations for allowed moves in the form of a separate ConcreteGame structure. To play the game, we could just build something on top of the type of states directly, if that makes sense.

[Violeta Hernández]

Kevin Buzzard said:

Re the README: are you sure Tic-Tac-Toe and chess are combinatorial games? I thought neither of them were played under the "normal play rule" ("you lose precisely when you can't move") and furthermore chess can go on forever unless you invoke the 50 move rule which again is not part of the normal play rule (and means that it's not true that the moves are determined by the position alone). Or is there some hack to make this true?

That's a fair point! You can turn any terminating game with ties into a combinatorial game by simply giving all ties to some specific player, though arguably that turns them into different games. I'll update the README with some better examples.

The case of tic-tac-toe is interesting because you can prove by a strategy stealing argument that a (m, n, k)-game can never be won by the second player. Which means, you can perform roughly the same analysis if you consider a variant of tic-tac-toe where ties are turned into second-player wins, even though that is a bit of a hack.

[Ilmārs Cīrulis]

CGT works only with finite/terminating games, right?

[Owen Randall]

Also, this repository might be of interest:
https://github.com/davidowe/MATH681CourseProject
It was a course project of mine which implements Chomp, Linear Clobber, and Hex based on the existing mathlib CGT framework

[Owen Randall]

Ilmārs Cīrulis said:

CGT works only with finite/terminating games, right?

Not necessarily. You need infinite games to construct the reals for example. What analysis you can do on infinite games I'm not exactly sure, but I'm pretty sure games need to be without cycles for CGT to apply.

[Aaron Liu]

CGT only applies to terminating games, where terminating means that any sequence of moves (ignoring normal turn order) will halt.

[Violeta Hernández]

Owen Randall said:

Also, this repository might be of interest:
https://github.com/davidowe/MATH681CourseProject
It was a course project of mine which implements Chomp, Linear Clobber, and Hex based on the existing mathlib CGT framework

This is very useful! We can already implement Chomp as a specific case of a poset game, but Hex and Clobber would be great to have!

[Violeta Hernández]

If you're interested in porting this material over, I can walk you through what's changed from the Mathlib implementation of games.

[Tristan Figueroa-Reid]

Kevin Buzzard said:

Re the README: are you sure Tic-Tac-Toe and chess are combinatorial games? I thought neither of them were played under the "normal play rule" ("you lose precisely when you can't move") and furthermore chess can go on forever unless you invoke the 50 move rule which again is not part of the normal play rule (and means that it's not true that the moves are determined by the position alone). Or is there some hack to make this true?

There is a hack: you can use loopy games which do consider draws. For games that halt on a draw, you can change them to play infinitely.

[Mario Carneiro]

Violeta Hernández said:

That's a fair point! You can turn any terminating game with ties into a combinatorial game by simply giving all ties to some specific player, though arguably that turns them into different games.

Not necessarily; for many game theory questions like "is there a winning strategy for player 1" you don't get 3 options anyway so the definition will naturally make draws act equivalently to a win for one of the players

[Mario Carneiro]

I think that also suggests a fairly straightforward definition for a game-with-ties, namely a pair of CGT games representing the game from each player's perspective (making ties go to the opponent), possibly together with a requirement that you can't win both games (a win for one player can't also be a win for the other)

[Aaron Liu]

Mario Carneiro said:

I think that also suggests a fairly straightforward definition for a game-with-ties, namely a pair of CGT games representing the game from each player's perspective (making ties go to the opponent), possibly together with a requirement that you can't win both games (a win for one player can't also be a win for the other)

This seems very similar to the setup for analyzing loopy games, maybe ties could be implemented as an infinite loop?

[Ilmārs Cīrulis]

Ties as infinite loop? In chess, for example, stalemates count as ties too, but I don't get how they can be interpreted as loops - as there is no more moves for stalemated player.

[Ilmārs Cīrulis]

Does making endgame databases count as part of CGT, too? (Using Mario Carneiro's approach, if necessary, with two games to take care of ties.) I'm kinda interested into some general form/definition of these, maybe I could contribute something. :thinking:

[Ilmārs Cīrulis]

Going to read the literature to learn more.

[Somo S.]

Kevin Buzzard said:

Yes I kind of realised the tic-tac-toe hack as I was writing. I can't really make it work for chess though. I think that in theory a game can go on forever? Don't the players actually have to agree on a draw after 50 moves, rather than it being forced on them?

I dont know what the state of the art is in this area these days, but I had learnt that if it can be proven that optimal play, by perfectly rational actors, leads to a provably infinite game of chess, then that game is a draw. E.g if the state of the board somehow has only got two kings each on the diagonally opposite corners of the board

[Mario Carneiro]

Ilmārs Cīrulis said:

Ties as infinite loop? In chess, for example, stalemates count as ties too, but I don't get how they can be interpreted as loops - as there is no more moves for stalemated player.

I think the point is that you can modify the move set such that once you enter a tie state, a magic extra move option becomes available. So if player 1 puts player 2 in stalemate, then player 2 has exactly one response which is to move to the "stalemate state", and both player 1 and player 2 have only one move in this state which does nothing. So termination becomes impossible once you enter the state

[Mario Carneiro]

By the way, you can do similar things to chess to accommodate rules like the 3 move rule or the 50 move rule, you just add additional state to keep track of how far you are in the game

[Mario Carneiro]

although I guess said extra state can't itself be used by the 3 move rule :)

[Aaron Liu]

You can make the "state" the entire history of the game.

[Kevin Buzzard]

yeah and then I think the relationship to CGT has become really tenuous: you are just saying "here's a regular game, it's actually a gigantic poset, now play the game on the poset" and none of the theory of CGT is going to be any use in practice (not that it's of much use in chess anyway!)

I once wrote a paper about how the applications of CGT to Dots and Boxes explained in WW were very tenuous in practice (in expert play on a 5x5 board). The point is that Dots and Boxes is also not played under the normal play rule; in WW they say "you may as well assume that it is" but this statement has not aged at all well.

[Kim Morrison]

I hope someone will just implement chess without any regard for the CGT setup. I started once long ago on branch#chess, trying to prove that two complete ranks of pawns could not pass each other. It has some mostly-proved theorems like "/-- If a pawn moves without taking, it does not change file. -/", and that after a move the number of pieces has changed by 0 or -1, etc.

[Violeta Hernández]

We could expand the scope of the repo to analyze games like chess, but since there's already a lot of things to prove as is this would not be a top priority.

[Vlad Tsyrklevich]

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

[Tristan Figueroa-Reid]

I think one thing that seems to be creeping on this topic is the distinction between analyzing/solving specific games (Chess, Tic-Tac-Toe) and the general theorems in CGT that apply to entire classes of games/games created specifically for easy analysis by CGT. It would make sense for there to be utilities for those positional games like Chess and Tic-Tac-Toe where the utilities we have can provably determine the winning outcome of those games, but, as aforementioned, CGT is not remotely equipped as a field to analyze any specific game that people normally play without extensive extra theory on top.

The current list of implemented games in the CGT Lean repository includes games that arose from the need for simple-to-analyze games.

[Aaron Liu]

I have a bunch of stuff from #Is there code for X? > ✔ `Surreal.mk` lemmas that I am ready to push, how should I contribute?

[Violeta Hernández]

Aaron Liu said:

I have a bunch of stuff from #Is there code for X? > ✔ `Surreal.mk` lemmas that I am ready to push, how should I contribute?

You can make a PR to the repository!

[Violeta Hernández]

Do note that most of the theorems you list (if not all?) already exist on the new repo.

[Violeta Hernández]

Oh, actually Surreal.mk_natCast was missing, but it's a very short proof so I just went ahead and PR'd it myself
https://github.com/vihdzp/combinatorial-games/pull/75

[Violeta Hernández]

I'm wondering, should we absorb docs#NatOrdinal into the CGT repository?

[Kevin Buzzard]

What is the motivation for natural addition and multiplication? Is it CGT? Definitely ordinals should be staying in mathlib (I think we're all agreed on that) but I've never heard of this variant. Hmm, judging by the docstring CGT looks like the application so I'd be happy with the move, and indeed it's only imported by stuff in Mathlib.SetTheory.Game

[Kevin Buzzard]

Off-topic: why make both the type synonym and the funky notation? Is that the notation used in the literature or something?

[Violeta Hernández]

Natural addition and multiplication arise chiefly in CGT as the addition and multiplication of ordinals as games, but they have some connection to well-ordered sets. For instance, the ordinal sum a + b is the order type of the lexicographic sum of a and b, while a # b is the greatest order type of any well-order c to which a and b have order embeddings covering the entire set.

There's also nice connections to the Cantor Normal Form: natural addition and multiplication correspond to adding and multiplying CNFs as if they were polynomials in omega. I've got a series of PRs proving this which have stalled for months...

[Violeta Hernández]

The notation is in use within the literature. My original idea was to have the operations defined on Ordinal for convenience, and just use the type alias NatOrdinal to transfer results resulting from the ordered semiring structure over. But in hindsight it would probably be nicer to just define the type alias, and make the notation a # b stand for toOrdinal (toNatOrdinal a + toNatOrdinal b).

[Violeta Hernández]

I guess the move to the CGT repo would make it easier to do this refactor.

[Aaron Liu]

Violeta Hernández said:

For instance, the ordinal sum a + b is the order type of the lexicographic sum of a and b, while a # b is the greatest order type of any well-order c to which a and b have order embeddings covering the entire set.

Why can't I find this anywhere in mathlib? We should have

Maximal (fun c ↦ ∃ (f : Iio a ⊕ Iio b →o Iio c), Function.Surjective f) (a ♯ b)

and

Maximal (fun c ↦ ∃ (f : Iio a × Iio b →o Iio c), Function.Surjective f) (a ⨳ b)

Also, why does ⨳ not have any abbreviation?

[Violeta Hernández]

You can't find it in Mathlib because I haven't proven it yet! But it would be a welcome addition to the CGT repo.

I recently learned that it's possible to define per-repo VSCode abbreviations, so we could have something like \nmul or simply \*# for ⨳.

[Mario Carneiro]

you could also contribute those to the global list, maintenance is generally quite happy to add symbols if they get use in any domain

[Violeta Hernández]

That's nice to hear. I remember getting some pushback from Yaël when I added \lf for ⧏.

[Mario Carneiro]

that was probably for using the symbol, not for registering it in abbreviations.json

[Mario Carneiro]

the only reason I would want to avoid putting something like that in abbreviations.json is if it's squatting a name that wants to be used for something else, or if it's a prefix of something else which is common

[Yaël Dillies]

It was for breaking the nice \lf, \rf, \lc, \rc series. Btw I still think we should revert it!

[Mario Carneiro]

ah, so both of the above then

[Violeta Hernández]

I'm not opposed to having that notation be exclusive to the CGT repo

[Alex Meiburg]

I saw this paper show up today: https://arxiv.org/abs/2503.16781
It's a fun idea, and the math is quite self-contained. I think trying to see how easily this can be directly dropped into the existing definitions would a cool test. It would be pretty neat if someone could say that they formalized a new paper within a few days of it coming out. :)

[Tristan Figueroa-Reid]

Actually, that does seem like a relatively short paper! I should be able to at the very least get some of the first few lemmas in today.

[Tristan Figueroa-Reid]

Stuck in a little bit of ConcreteGame problems, but I should mention that the base game is formalized (decidability for moves was a little annoying)