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)

[Wrenna Robson]

@Violeta Hernández I should say I am no kind of combinatorial game theorist, but bearing that in mind, are you still looking for contributors?

[Violeta Hernández]

We are!

[Violeta Hernández]

The repo died down a bit when I went on hiatus, but we're back to full steam :heart:

[Wrenna Robson]

I am interested.

[Aaron Liu]

excited to see what you will contribute

[Tristan Figueroa-Reid]

I've been having some trouble using this definition (specifically, I can case-crunch through a proof of birthday_unreverse_le, but I'm having trouble using aesop with it):

/-- Unreversing a game. -/
noncomputable def unreverse (x : IGame) : IGame :=
  let l := { y : Set.range fun z : x.leftMoves ↦ unreverse z | ∃ z ∈ y.val.rightMoves, z ≤ x }
  let r := { y : Set.range fun z : x.rightMoves ↦ unreverse z | ∃ z ∈ y.val.leftMoves, x ≤ z }
  {(⋃ y : l, y.prop.choose.leftMoves) ∪ Subtype.val '' lᶜ |
    (⋃ y : r, y.prop.choose.rightMoves) ∪ Subtype.val '' rᶜ}ᴵ
termination_by x
decreasing_by igame_wf

Though, I do have trouble with definitions. What can I do better with here?

[Violeta Hernández]

(hey, currently completely invested in minimizing the surreal birthday proof, I'll think about this a bit later)

[Aaron Liu]

Tristan Figueroa-Reid said:

I've been having some trouble using this definition (specifically, I can case-crunch through a proof of birthday_unreverse_le, but I'm having trouble using aesop with it):

/-- Unreversing a game. -/
noncomputable def unreverse (x : IGame) : IGame :=
  let l := { y : Set.range fun z : x.leftMoves ↦ unreverse z | ∃ z ∈ y.val.rightMoves, z ≤ x }
  let r := { y : Set.range fun z : x.rightMoves ↦ unreverse z | ∃ z ∈ y.val.leftMoves, x ≤ z }
  {(⋃ y : l, y.prop.choose.leftMoves) ∪ Subtype.val '' lᶜ |
    (⋃ y : r, y.prop.choose.rightMoves) ∪ Subtype.val '' rᶜ}ᴵ
termination_by x
decreasing_by igame_wf

Though, I do have trouble with definitions. What can I do better with here?

what is this?

[Tristan Figueroa-Reid]

Aaron Liu said:

Tristan Figueroa-Reid said:

what is this?

unreverse x has no reversible moves.

[Tristan Figueroa-Reid]

@Aaron Liu thanks for the reversible/bypass proofs! :+1: I do suspect that the dominated result is too weak to help in some (recursive) canonical definition, but I think it's nice to keep on its own. Should we merge this with Canonical.lean?

[Tristan Figueroa-Reid]

(I'll do some golfs of equiv_of_bypassand equiv_of_gift)

[Tristan Figueroa-Reid]

Tristan Figueroa-Reid said:

(I'll do some golfs of equiv_of_bypassand equiv_of_gift)

For all of the lemmas that use left/right set membership, do we want accompanying lemmas about ofSets?

[Violeta Hernández]

@Aaron Liu @Tristan Figueroa-Reid Just wrote down my version of the surreal birthday proof a bit more nicely and with more detail: https://mathoverflow.net/a/497645/147705

[Violeta Hernández]

I think this should be straightforward to port into Lean. All the material on small cuts could probably go on the Dedekind file itself - the fact that cuts of games are small might reasonably come up again.

[Violeta Hernández]

I would like for us to switch to the Concept definition of Cut before we do that, though.

[Violeta Hernández]

@Tristan Figueroa-Reid For "context", see docs#Concept. You can sort of think of a concept as a really wide generalization of Dedekind cuts. In this case, a surreal gap is Concept Surreal Surreal (. < .).

[Violeta Hernández]

By using that definition we get that they're a complete lattice for free, and a linear order with little further work

[Violeta Hernández]

Just to make sure. We don't consider it acceptable to use the extent/intent terminology in the CGT repo, do we?

[Aaron Liu]

I would rather not

[Aaron Liu]

we should have a left/right or a lower/upper or anything that gives a sense of which one they are wrt the order

[Violeta Hernández]

It's slightly annoying to have to create a wrapper for it, but it's still easier than developing everything from scratch

[Violeta Hernández]

(deleted)

[Violeta Hernández]

I agree with left/right

[Violeta Hernández]

I've realized that I really don't actually need the definition of small sets in my surreal birthday proof. You can define the birthday of any cut, just setting the birthday of non-small cuts to ⊤ : WithTop NatOrdinal. As it happens, using this definition, you can still follow through the entire argument.

[Violeta Hernández]

So I think I'll close the PR on small cuts. I just want to make sure that what I'm saying is true, first

[Violeta Hernández]

I did it!
image.png

[Violeta Hernández]

The new proof isn't actually that much shorter compared to the old one, the file is just under 300 lines long

[Violeta Hernández]

But it should be much easier to follow, and it gives a lot of interesting side lemmas

[Violeta Hernández]

Opened a PR for this: https://github.com/vihdzp/combinatorial-games/pull/132

[Violeta Hernández]

I've been thinking about our definition of surreal cuts birthdays. The fact that it can be used in our result x.toGame.birthday = x.birthday suggests some amount of naturality to the definition.

[Violeta Hernández]

The way I define it in the PR is admittedly a bit artificial, coming from infima of only left cuts of surreals, or suprema of only right cuts of surreals. Though as it happens, you can actually lift the left/right cut restriction and get exactly the same values.

[Violeta Hernández]

This follows from my result on #134, as well as the fact that the birthday of a supremum/infimum is at most the supremum of the birthdays

[Violeta Hernández]

I've got a conjecture which I think might be interesting: the birthday of a cut is a limit ordinal iff it is not a left/right cut of a surreal

[Violeta Hernández]

The ← direction follows from the result I just proved.

[Violeta Hernández]

(the only cuts with birthday 0 are top and bot, which are not cuts of surreals, so that's some more fire for the eternal "is 0 a limit ordinal" debate)

[Violeta Hernández]

Oh, I think it's true! It can be showed with the auxiliary lemma I used to prove the result about birthdays of suprema/infima. oops proof doesn't work

[Violeta Hernández]

I'm glad Lean exists, I make way too many mistakes :rolling_on_the_floor_laughing:

[Violeta Hernández]

Can we prove Game.birthday (nim o) = o?

[Aaron Liu]

This is provable probably

[Aaron Liu]

Do you want me to do it?

[Tomasz Maciosowski]

Hey folks!

I am no CGT or Lean expert by any means, but I am interested in Misere play and was able to prove some results from Siegel here, so I was wondering if that's something you'd like to host in the repo as well, or if you're mostly interested in ONAG/normal play results then it's fine as well!

Talking about overlap, IGame is very useful to me (to talk about exact game forms) but without the notion of LE (it's a bit more involved in Misere and you usually want to do comparisions modulo some set cause otherwise there's not that many interesting results) and multiplication (just isn't really used). Also birthdays are quite useful at least to prove termination when you recurse on negations of subpositions.

[Aaron Liu]

Violeta Hernández said:

Can we prove Game.birthday (nim o) = o?

to do this I need a Game-valued version of nim (nim is IGame-valued)

[Violeta Hernández]

Aaron Liu said:

Violeta Hernández said:

Can we prove Game.birthday (nim o) = o?

to do this I need a Game-valued version of nim (nim is IGame-valued)

Well what I mean by this is Game.birthday (.mk (nim o)) = o.toOrdinal.toNatOrdinal, I was just trying to abbreviate things

[Aaron Liu]

I am trying now

[Aaron Liu]

it is quite difficult so I might need to give up for now and try to prove it informally first

[Violeta Hernández]

Yeah I spent a while thinking about this to no success

[Aaron Liu]

did you make any progress though

[Aaron Liu]

doesn't need to be outright success

[Violeta Hernández]

Well, I had the idea to define left/right Grundy values for non-impartial games. By a simple induction any game satisfies that the left/right Grundy values are bounded by the birthday. But these notions don't really seem to mean much for non-impartial games, or at the very least I haven't been able to link them to any order relations.

[Violeta Hernández]

An idea on a similar vein was to define some operation to turn a game equivalent to nim impartial, perhaps by copying the left set of moves to the right one, removing any options not equivalent to impartial games themselves, and repeating the process inductively. I haven't explored that too much yet.

[Violeta Hernández]

Here's a conjecture: if a game {xL | xR} is equivalent to an impartial game, then the game {xL | xL} is too, and equals the same game.

[Aaron Liu]

Falsified by {-1 | 1}

[Violeta Hernández]

Hmm... maybe {xL | -xL} then?

[Violeta Hernández]

Yeah that seems like a much more reasonable conjecture

[Aaron Liu]

this is true and I have a proof sketch

[Violeta Hernández]

I'm wondering if we could use this to prove the result on birthdays. This shows that in some way you only really need to focus on either the left or right sets of moves in order to build up a game equivalent to an impartial one.

[Aaron Liu]

it turns out to just be a follow-your-nose proof

example {i : IGame} (hi : i ≈ -i) : {i.leftMoves | -i.leftMoves}ᴵ ≈ i := by
  constructor
  · apply hi.right.trans'
    refine le_iff_forall_lf.2 ⟨fun z hz => ?_, fun z hz => ?_⟩
    · rw [leftMoves_ofSets] at hz
      refine not_le_of_not_le_of_le ?_ hi.left
      exact leftMove_lf hz
    · rw [rightMoves_neg] at hz
      apply lf_rightMove
      rwa [rightMoves_ofSets]
  · refine le_iff_forall_lf.2 ⟨fun z hz => ?_, fun z hz => ?_⟩
    · apply leftMove_lf
      rwa [leftMoves_ofSets]
    · rw [rightMoves_ofSets] at hz
      apply not_le_of_le_of_not_le hi.left
      apply lf_rightMove
      rwa [rightMoves_neg]

[Tristan Figueroa-Reid]

@Tomasz Maciosowski I think it would be worthwhile thinking of a more algebraically-motivated auxillary definitions of misère games over the current ones formulated through play.

[Tomasz Maciosowski]

Generally that's quite an interesting topic. Starting with normal play:

I know that your definition for LE matches with what Conway is doing in ONAG, and is still used in Winning Ways, but that's not really the definition that modern CGT is using. I'm not sure when exactly the change happened but already the first edition of "Lessons in Play" (2007) defines it as (p. 71)

$$G \ge H \text { if } \forall X \text{ Left wins } G + X \text{ whenever Left wins } H + X$$

which basically boils down to $G \ge H \Leftrightarrow \forall X. o(G + X) \ge o(H + X)$ like Siegel is defining it (p. 57, definition 1.16) and in the modern literature Conway's definition is a consequence of the definition via outcome classes that can be proven to hold.

Also worth mentioning that current literature would rather define $=$ using outcome classes as well rather than antisymmetrization on $\ge$ i.e. $G = H \Leftrightarrow \forall X. o(G + X) = o(H + X)$ (Siegel, p. 55, Definition 1.7)

I'd say that both approaches are fine and it depends on what you're actually aim to formalize (ONAG or "modern" CGT)

Now in misere we can use the same definition, swapping $o$ for $o^-$, and I haven't really seen anybody using any other definition for misere. That definition is quite useful for formalizing recent developments about misere universes cause it can be easily augmented to $G =^-_{A} H \Leftrightarrow \forall (X \in A). o^-(G + X) = o^-(H + X)$ which now defines inequality modulo $A$ (Rebecca Milley's thesis, p. 9, Definition 2.1.6)

Generally in misere there's not much algebraic results (non restricted misere is not only not a group but also no element has an inverse) thus the work to get to the universes part where we start to have something

[Aaron Liu]

My only references right now are ONAG and Winning Ways so

[Tomasz Maciosowski]

I've also found this paper by Siegel that pre-dates Lessons in Play by a couple months that's also using outcome definition of game equality in normal play.

2nd edition of Lessons in Play quite nicely also defines the outcome function in terms of outcomes for Left and Right players ($o_L$ and $o_R$) (p. 37, Definition 2.4) which is more or less what I was following for my definitions

[Tristan Figueroa-Reid]

Thanks for the background info! It is a little saddening that Misère games don't have many interesting algebraic properties. [Since I never explored misère games, I was optimistically hoping that there were some nice algebraic properties I didn't know about.] I've been under the belief that defining (normal-play) games algebraically is much more appealing, especially from a formalization perspective, though adding Misère games definitely necessitates some kind of Outcomes file for general IGames. Regardless, I would still love to see Misère games be part of the main combinatorial-games branch!

[Tomasz Maciosowski]

Yeah, I'd say that non-restricted misere doesn't have much algebraic structure (not even not a group, _nothing_ has inverse!), but there are nice results that could be formalized once you have universes and probably augmented forms as well as you need them for some proofs. Absolute Combinatorial Game Theory is a good first read

[Violeta Hernández]

I know nothing about Misère play but I'm very willing to learn!

[Violeta Hernández]

I'd love to see some PRs to the main branch

[Tristan Figueroa-Reid]

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?

Was reminded of this today - GamesCrafters has a website for playing some combinatorial games.

[Violeta Hernández]

I think it'd be fun if we could play more "abstract" games as well, like 11/8 or *5

[Aaron Liu]

I think it would be fun if we could write proofs by playing games

[Tristan Figueroa-Reid]

Violeta Hernández said:

I think it'd be fun if we could play more "abstract" games as well, like 11/8 or *5

This might be made relatively straightforward with ProofWidgets

[Tristan Figueroa-Reid]

Aaron Liu said:

I think it would be fun if we could write proofs by playing games

Something like TwoFx/sudoku or lean4-maze?

[Django Peeters]

Hello everyone!

I am interested in contributing to this repository and would like to join.
At the moment I'm focussing on Nimbers and have been using HW Lenstra Jr's On the algebraic closure of two and Nim multiplication, besides ONAG.

[Tristan Figueroa-Reid]

Does anyone know of efficient ℕ → [Short] IGame bijections? (ℤ or finite tuples are fine instead of ℕ.) I can only come up with efficient surjections, or very inefficient bijections. (In practice, for Plausible, I don't think efficiency practically matters, but I would like to formalize a beautiful function rather than hack my way through some of my current ideas)

[Aaron Liu]

What do you mean by efficient?

[Tristan Figueroa-Reid]

Aaron Liu said:

What do you mean by efficient?

Just computationally efficient proportional to the input ℕ. I've only come up with exponential ways to generate short IGames directly, or finicky ways to turn trees into game trees that feel very unnatural. Heuristically, I would like something that isn't recursive.

[Aaron Liu]

ofSets is noncomputable, how do you want to compute these IGames?

[Violeta Hernández]

Tristan Figueroa-Reid said:

Does anyone know of efficient ℕ → [Short] IGame bijections? (ℤ or finite tuples are fine instead of ℕ.) I can only come up with efficient surjections, or very inefficient bijections. (In practice, for Plausible, I don't think efficiency practically matters, but I would like to formalize a beautiful function rather than hack my way through some of my current ideas)

Write n in base 4. It's kth digit determines whether the kth set in the bijection goes on the left set, right set, none, or both.

[Aaron Liu]

that works I guess

[Tristan Figueroa-Reid]

Violeta Hernández said:

Write n in base 4. It's kth digit determines whether the kth set in the bijection goes on the left set, right set, none, or both.

You get surjectivity but not injectivity. If 0 mapped to the left set, then 00 would mean the 1st and second set both went to the left, which falls under the same IGame equivalence class.

[Aaron Liu]

let digit zero mean mapped to neither set

[Aaron Liu]

problem solved

[Violeta Hernández]

As a bit of a historical note, I first learned of an analogous bijection to enumerate hereditarily finite sets

[Tristan Figueroa-Reid]

0 was a bad pick. If you take the digit that goes to the left set, repeating that twice gives you the same one.

[Aaron Liu]

give an example

[Violeta Hernández]

Yeah, I think this construction should work as long as 0 means "it goes in neither set".

[Aaron Liu]

ok I'll give an example
37, which is 211 in base 4. This means the 0th game on the left, the 1st game on the left, and the 2nd game on the right.
the 0th game is 0
the 1st game is the one with the 0th game on the left
the 2nd game is the one with the 0th game on the right
so you get {0, {0 |} | {| 0}}

[Tristan Figueroa-Reid]

Great. I do wish there was something that wasn't recursive, but I guess I'm asking a lot from a field which notoriously uses a lot of recursive constructions.

[Violeta Hernández]

Well, if we're already going to allow native_decide for use with FGame, I don't see the issue.

[Aaron Liu]

what's an FGame

[Violeta Hernández]

An auxiliary type Tristan made specifically for repl/computability purposes

[Violeta Hernández]

The F stands for Finset

[Aaron Liu]

so it only does short games?

[Violeta Hernández]

Yep

[Violeta Hernández]

By the way, how exactly is the Plausible integration going to work? What kinds of statements would work with it? (Or more generally, how does Plausible work in general?)

[Violeta Hernández]

I wanted to PR some more stuff to FGame but I'm not actually sure how much we actually need to develop the type

[Tristan Figueroa-Reid]

We do need to re-make any definitions from IGame that aren't computable already, unfortunately. I don't understand how Plausible knows what instances to synthesize when given hypotheses other than ∀ g : FGame, (_ : Decidable _), but it otherwise acts as your regular property tester (so to add integration, all we need is some random sampler on FGame and an optional shrinker.)

[Tristan Figueroa-Reid]

I'm not sure how extensive the property tester is, so I'm not sure if there are any genuine performance concerns with how fast our FGame generator is, but I could just cap the ℕ we sample at some value that works well enough for our use case.

[Violeta Hernández]

Correct me if I'm wrong, but I imagine it'd work like this. You first take a logical statement on IGame, and plug in toIGame x, toIGame y, ... You then use some simp set to turn this into an equivalent statement in terms of FGame. You then use native_decide to verify whether it's true or not. Repeat.

[Violeta Hernández]

Tristan Figueroa-Reid said:

We do need to re-make any definitions from IGame that aren't computable already, unfortunately. I don't understand how Plausible knows what instances to synthesize when given hypotheses other than ∀ g : FGame, (_ : Decidable _), but it otherwise acts as your regular property tester (so to add integration, all we need is some random sampler on FGame and an optional shrinker.)

Basically nothing in IGame is computable, because ofSets isn't computable (and it's much nicer to use it even with definitions such as 0 or 1 rather than trying to pass through PGame).

[Violeta Hernández]

I have efficient FGame negation on a branch of mine, as well as addition. I'll add multiplication to that list and make a PR.

[Tristan Figueroa-Reid]

After I review your PRs in a bit, I'll formalize your counting bijection and use that for plausible.

[Violeta Hernández]

(It's perhaps worth noting that multiplication is and will always be basically unworkable. I don't have a proof for this, but I think the size of the game tree can scale exponentially in the worst cases).

[Violeta Hernández]

Django Peeters said:

Hello everyone!

I am interested in contributing to this repository and would like to join.
At the moment I'm focussing on Nimbers and have been using HW Lenstra Jr's On the algebraic closure of two and Nim multiplication, besides ONAG.

There's a lot of progress on nimbers in the repo already, we've defined all the way up to the field structure. We still haven't shown that they're algebraically closed, but Daniel Weber and I have an unfinished proof that runs through Conway's argument.

[Violeta Hernández]

Are there any other results on nimbers you'd like to formalize?

[Violeta Hernández]

I think it'd be nice to show nimbers below w^w^w are algebraically closed as well, Lenstra's paper sketches that argument out I think.

[Violeta Hernández]

Something else I'd like to see is computable nimber arithmetic below w. Nim addition is nothing more than Nat.xor, so really it'd just be a matter of defining multiplication.

[Django Peeters]

I'm trying to understand how multiplication below w^w^w works using the alphas in Lenstra's papers as we speak. To this end I am in the middle of writing some python code to try examples and calculate more alphas, but I'm definitely interested in doing this in Lean.

[Violeta Hernández]

Aaron Siegel computed values up to 200 or so at my request a few months ago

[Violeta Hernández]

I'm not sure if he ever submitted them to OEIS. If they're not there, they should be somewhere in the cgsuite source code.

[Django Peeters]

You're right, I found the program. I do have cgsuite so maybe it'll be a waste of time to reimplement it in python lol.

[Violeta Hernández]

I don't know the algorithm to compute these alpha values, but perhaps it could be a good idea to implement it in C if for no other reason than to eek out a bit more performance.

[Tomasz Maciosowski]

Violeta Hernández said:

I'd love to see some PRs to the main branch

I've opened a first PR that upstreams outcome definitions, later can upstream adjoints that depend on that one and this should be enough separated building blocks to upstream that there are no inverses in misere.

Also, that's my first substantial lean contribution so I'm open for feedback!

[Violeta Hernández]

I'll review it shortly!

[Violeta Hernández]

We have a lot of activity in this thread, I wonder if it might be time to ask for our own channel

[Violeta Hernández]

@Tomasz Maciosowski Left a review on your PR. Hope I don't come off as harsh, the contribution of misère play is quite welcome!

[Violeta Hernández]

Btw, I was thinking about a completely different approach to implementing misère play. What do you think about this?

/-- Play a game using a misère convention. That means, every subposition that previously had no
moves for a given player now has a single move to `0`, granting them the win. -/
def toMisere (x : IGame.{u}) : IGame.{u} := by classical exact
  {if x.leftMoves = ∅ then {0} else (range fun y : x.leftMoves ↦ toMisere y) |
    if x.rightMoves = ∅ then {0} else (range fun y : x.rightMoves ↦ toMisere y)}ᴵ
termination_by x
decreasing_by igame_wf

[Aaron Liu]

interesting

[Violeta Hernández]

(let me just prove correctness of this real quick, I might be saying nonsense!)

[Violeta Hernández]

Yep, check this out!
https://github.com/vihdzp/combinatorial-games/blob/vi.misereTest/CombinatorialGames/Game/Misere.lean

[Violeta Hernández]

In particular:

/-- Left wins as the first player iff they run out of moves, or if there's some move that right
can't win as the first player. -/
theorem zero_lf_toMisere {x : IGame} :
    0 ⧏ toMisere x ↔ x.leftMoves = ∅ ∨ ∃ y ∈ x.leftMoves, 0 ≤ toMisere y := sorry

/-- Right wins as the first player iff they run out of moves, or if there's some move that left
can't win as the first player. -/
theorem toMisere_lf_zero {x : IGame} :
    toMisere x ⧏ 0 ↔ x.rightMoves = ∅ ∨ ∃ y ∈ x.rightMoves, toMisere y ≤ 0 := sorry

Note that these are the same definitions as LeftWinsGoingFirst and RightWinsGoingFirst!

[Violeta Hernández]

The advantage of doing this is that we don't need to make any new outcome machinery, as we can simply use the order relations on toMisere x to state which player wins

[Violeta Hernández]

Also, we can now do:

def MisereEQ (A : IGame → Prop) (g h : IGame) : Prop :=
  ∀ x, A x → toMisere (g + x) ≈ toMisere (h + x)

def MisereLE (A : IGame → Prop) (g h : IGame) : Prop :=
  ∀ x, A x → toMisere (g + x) ≤ toMisere (h + x)

[Violeta Hernández]

Re: #general > Combinatorial game theory repository @ 💬
The definition you give for $G \ge H$ is definitely a nicer one conceptually, and it's the one I'd use in a teaching setting. But I don't really know how you'd be able to prove any concrete inequality (say 2 ≤ 4) without first proving the definition in terms of options

$$G \ge H \leftrightarrow (\forall G^L, G^L \not\ge H) \land (\forall H^R, G \not\ge H^R).$$

Also, I think the difference between using order relations and outcome relations is but a notational one (in normal play). You could presumably do something like:

macro_rules | `(LeftWinsAsSnd $x) => `(0 ≤ $x)
macro_rules | `(RightWinsAsSnd $x) => `($x ≤ 0)
macro_rules | `(LeftWinsAsFst $x) => `(¬ $x ≤ 0)
macro_rules | `(RightWinsAsFst $x) => `(¬ 0 ≤ $x)
macro_rules | `(LeftWins $x) => `(0 < $x)
macro_rules | `(RightWins $x) => `($x < 0)

Then all relevant basic results on outcomes would be spelled out verbatim by our theorems zero_le, le_zero, zero_lf, and lf_zero, as well as the more general theorem on preorders lt_iff_le_not_ge. Of course, this would make the order structure of games much less transparent.

[Tristan Figueroa-Reid]

(Should we open a new thread in general about a combinatorial game theory channel?)

[Violeta Hernández]

(Sure!)

[Violeta Hernández]

I'm reading Absolute combinatorial game theory, and I can definitely see how your implementation of misère games mirrors that paper. I would like to point out something important: IGame cannot represent scoring play, since all outcomes are only distinguished via extensionality. I'd love to see the ideas from this paper formalized, but perhaps that should be done separately from what we're doing with IGame.

[Violeta Hernández]

(something similar applies to loopy games, we'll eventually have to define a new data type to represent those as well!)

[Tomasz Maciosowski]

Violeta Hernández said:

Btw, I was thinking about a completely different approach to implementing misère play. What do you think about this?

/-- Play a game using a misère convention. That means, every subposition that previously had no
moves for a given player now has a single move to `0`, granting them the win. -/
def toMisere (x : IGame.{u}) : IGame.{u} := by classical exact
  {if x.leftMoves = ∅ then {0} else (range fun y : x.leftMoves ↦ toMisere y) |
    if x.rightMoves = ∅ then {0} else (range fun y : x.rightMoves ↦ toMisere y)}ᴵ
termination_by x
decreasing_by igame_wf

Hm that's quite interesting, I wonder if that's easier to work with in the proofs. However, I'm not actually sure if using that as the definition is the way to go when formalizing results, at the end literature is using the definition via outcomes so I feel like that should be the "canonical" one and if this one proves being more useful then have an iff proof that they're equivalent. I guess the real test will trying to use it to prove (g =m AnyGame 0 ↔ g = 0). I've followed Siegel's paper proof quite closely and the reasoning about outcomes and responses to Left/Right moves translated to lean proof verbatim

Violeta Hernández said:

I would like to point out something important: IGame cannot represent scoring play, since all outcomes are only distinguished via extensionality

Yeah, I'm aware. That also applies to extended forms (ones with tombstones) that aren't useful on their own but they're used for a couple of proofs that we don't have proofs without using them (yet, some folks are interested in that)

[Violeta Hernández]

Again, I don't really think we need definitions of outcomes, at least when working within IGame. The order relations of a game with 0 already encode this information, and any proof of this boils down to a thinly veiled tautology.

[Django Peeters]

Violeta Hernández said:

(something similar applies to loopy games, we'll eventually have to define a new data type to represent those as well!)

How about a pointed, directed graph where the directed edges can only have 1 of 2 colours, where the chosen point is a vertex representing the starting position.

[Aaron Liu]

Django Peeters said:

Violeta Hernández said:

(something similar applies to loopy games, we'll eventually have to define a new data type to represent those as well!)

How about a pointed, directed graph where the directed edges can only have 1 of 2 colours, where the chosen point is a vertex representing the starting position.

I have a work in progress definition of loopy games as a subquotient of countably deep u-small branching trees

[Aaron Liu]

It's tricky since the trees are coinductive so I have to build them up with a series of approximations

[Django Peeters]

Countable because a play always has a countable number of steps I guess?

[Violeta Hernández]

We have our own channel now! Please post about any future topics over there: #combinatorial-games