Combinatorial and positional game theory in Lean

Stream: general

[Yves Jäckle]

Hello!
I've worked on some combinatorial and positional game theory at : https://github.com/Happyves/Lean_Games
I've formalized Zermelo's theorem, the notions of strategy stealing, of positional games and of pairing strategies, and I've applied them to the games of Pick-up-bricks, Chomp, and Tic-tac-toe.
I'm still working on some aspects, though the versions in the folder "gameLib" and "games" are compiling and documented (but the API needs major cleaning and refactoring).

It is quite unfortunate, but these topics are closely related to the recently announced formalization of Gale Stewart games:
#announce > Borel determinacy
Perhaps we can unite the formalisms ?
@Sven Manthe

[Sven Manthe]

I just had a very short look at your project. If I didn't misunderstand something, you are just formalizing finite time games. I don't think these results could be used to simplify anything in my project. The other way around, you could of course try to map your games to Gale-Stewart games to

1. derive Zermelo's theorem from Borel (or even just closed) determinacy instead of your direct proof, and/or
2. provide formalizations of your specific games, e.g. Chomp, as Gale-Stewart games.

Let me also mention that most of my code really is dedicated to proving Borel determinacy itself and not to provide a nice API for games. Thus, it may be interesting to

3. add such API (e.g., reducing games with more than two possible outcomes to my notion of games, the most powerful formalism known to me being Blackwell games).

However, this would probably be orthogonal to the applications in descriptive set theory that are most interesting to me personally.
If there are further connections between our projects, or you have specific plans to unite something, I'd be happy to discuss them.

[Yves Jäckle]

I added an article to help read through the project : https://github.com/Happyves/Lean_Games/blob/master/GTarticle.pdf

@Kim Morrison (tagging you here as the most frequently appearing author in SetTheory/Game)
I wanted to ask about the option of including the work of Sven and mine in Mathlib. Of course, the inclusion may come under a set of conditions and refactors. My work is in desperate need of cleaning, for example.
The work in SetTheory/Game perfectly formalizes combinatorial games in the sense that Conway defined them. I come from a background in which very concrete games are studied, such as Shannon's switching game and more generally positional games, or cops and robbers on graphs. I found it difficult to express these games in Conway's formalism, as well as key proof arguments such as strategy stealing and pairing strategies.
I therefore wanted to ask whether mathlib would be open to a new additional formalism for this kind of game theory. Sven seems interested in game theory from the set theoretical perspective, and I am interested from the combinatorics perspective. Game theory naturally comes in many flavors, which is why I don't believe it to be problematic to have different notions of games in the library. In fact, it is probably a very interesting topic to figure out whether the formalisms in SetTheory/Game, those of Sven and mine, are related and how. And even with these formalisms, we have still more topics to cover, such as alpha-beta-pruning.

I understand you (Kim) are a person with many duties and I - and I assume Sven as well - will do my best to contribute in such a project. @Yaël Dillies is aware of my project and would be interested in reviewing PRs for a possible mathlib integration.

[Sven Manthe]

Let me just add that Gale-Stewart games, which I formalized, are not a particular case of Conway's games (and part of the usual graduate textbooks on descriptive set theory, so probably should become part of mathlib at some point)

[Kim Morrison]

I'm not at all an expert in this stuff: most of what I formalized in Mathlib about Conway's games I learnt as I was formalizing...

But yes, I absolutely agree that there is more to game theory than Conway's formalism, that this is appropriate material for Mathlib, and that someone should work out how to add other formalisms. The usual caveat: it's incredibly hard to come up with good definitions!

[Yves Jäckle]

Wonderful :tada: !
I'll start by PRing my lemmata about Lists. In parallel, I'll try to conclude my experiments with conditioning strategies on histories being neutral, and I'll try to find connections between the formalism of PGame, those of Sven and mine.

[Daniel Weber]

Please write here when you make these PRs, I'm interested in that

[Joseph Myers]

Certainly adding different notions of games to mathlib makes sense (along with various well-known individual games) - the idea of "game" is probably too general to expect that any one notion can usefully cover everything.

I've thought quite a bit about what uniform conventions for consistently formalizing competition problem statements, for use as challenges for AIs (challenging AIs to solve the problems, or to autoformalize informal proofs), should look like. For problems involving games my conclusion is that ad hoc definitions for each specific problem are more appropriate than trying to fit things into a very general formalism - even if an occasional problem does fit in such a formalism, it would be better (in the context of challenging AIs on problems originally set for humans) for it to be formalized consistently with others that don't fit in such a formalism (and also consistently with those competition problems involving a sequence of choices of operations to be made with perfect information, which can be thought of as single-player games).

Of course an AI would be free to use more general theory from mathlib in its solution if it so wishes. And because games allow expressions of the same problem that look so different in Lean, there might be scope for an AI challenge of the form "prove these two very different expressions of this problem are in fact equivalent". (An AI that could do that kind of thing would be of obvious practical use, considering how often in formalization you find you need to write a translation between different ways of expressing the same mathematical idea.)

Concrete problems that do fit in very general formalisms for the notion of "game" may also serve as useful challenges for humans to show that a general formalism is actually usable for concrete results on such problems.

[Violeta Hernández]

I disagree that this is something separate from Conway's formalism. Chomp, Tic-tac-toe, and really any finite time game should perfectly fit within our PGame definition.

[Violeta Hernández]

If the issue is the layer of abstraction, then perhaps we just need better API.

[Violeta Hernández]

Here's a sketch for formalizing Tic-tac-toe as a PGame. First, you can define an auxiliary type for Tic-tac-toe game states. Then you can define the subsequency relation for both players, determining which game states can be immediately attained by the next player in a single move, given another game state. Then prove this relation is well-founded (which should be easy since each move decreases the number of available squares). Finally, the definition for Tic-tac-toe will look something like

def ticTacToe (state : TicTacToe) : PGame :=
  .mk state.leftSubsequent state.rightSubsequent
  (fun x => ticTacToe x) (fun x => ticTacToe x)
termination_by state

[Violeta Hernández]

In fact I was planning on doing this for the poset game (a generalization of chomp) but got stuck due to a lack of a PartiallyWellOrdered predicate on types (this condition is necessary to prove termination in finite time).

[Violeta Hernández]

Something I think would be a good idea to implement within Mathlib is an auxiliary type like Game_World which minimizes the boilerplate in turning a "concrete" game into a PGame. I think we can boil the definition down to the following: a type of states, and two well-founded relations which determine how both players can change states.

[Violeta Hernández]

We at some point had definitions like PGame.Winning, PGame.Losing, etc. which determined whether a game could be won or lost by a given player. I refactored them out since they were nothing more than x > 0, x < 0, etc. But if they're helpful in removing a layer of abstraction we could bring them back as abbrevs or something.

[Violeta Hernández]

Game theory is fragmentary enough as it is and I don't think it helps Mathlib's purpose of unifying mathematics to fragment it any further.

[Violeta Hernández]

Violeta Hernández said:

Something I think would be a good idea to implement within Mathlib is an auxiliary type like Game_World which minimizes the boilerplate in turning a "concrete" game into a PGame. I think we can boil the definition down to the following: a type of states, and two well-founded relations which determine how both players can change states.

Here's a proof of concept of my idea: https://github.com/leanprover-community/mathlib4/compare/master...vi.concreteGame

[Violeta Hernández]

In my implementation of ConcreteGame I don't enforce any condition that turns be alternating. If we wanted, we could implement another layer of abstraction on top, e.g. AlternatingTurnGame α β, which describes the game states α and β for both players. Then an AlternatingTurnGame α β could be turned into a ConcreteGame (α ⊕ β).

[Violeta Hernández]

What do you think about all this?

[Yves Jäckle]

PGame3.lean
I'm currently working on connecting the Conway formalism and mine.
Here's my progress

[Yves Jäckle]

What I find difficult in the Conway formalism is that the notion of a strategy is quite implicit.
The game theory I'm interested in has many results of the form: "for some special cases of parameters determining the game, the game does have a winning/drawing strategy for player x". For example, for d-dimensional tic tac toe on a cube of length n, we can show that if n > 3^d - 1, the players have drawing strategies.
Building these strategies requires being able to define them quite directly. For example, for d-dimensional tic tac toe on a cube of length n, the trick is that for n > 3^d - 1, each combinatorial line (the set a player has to fill out to win) will contain a pair of points, so that all points considered are distinct. Then, the drawing strategy consist in selecting the opposite point of a pair whenever the opponent has selected one in the previous turn. (This is easly said, but not so easy to express in a formal context)
I'm not claiming the example above can't be expressed in Conway's formalism. I believe it makes proofs easier to have strategies be functions mapping lists of prior moves to moves to play. I'm in no way saying that the Conway formalism is pointless: it is required to derive the surreal numbers ! As I posted above, I believe it would be possible to connect the two formalisms.

[Yves Jäckle]

Violeta Hernández said:

Here's a proof of concept of my idea: https://github.com/leanprover-community/mathlib4/compare/master...vi.concreteGame

I'm happy to see you're working on the subject too !

[Violeta Hernández]

In Conway's formalism,

Yves Jäckle said:

Building these strategies requires being able to define them quite directly. For example, for d-dimensional tic tac toe on a cube of length n, the trick is that for n > 3^d - 1, each combinatorial line (the set a player has to fill out to win) will contain a pair of points, so that all points considered are distinct. Then, the drawing strategy consist in selecting the opposite point of a pair whenever the opponent has selected one in the previous turn. (This is easly said, but not so easy to express in a formal context)

The usual way to envision a strategy is "if a player always replies to a game state with a given move, they will preserve some invariant, which implies they will never run out of moves, which implies they win". I think that in order to work with Conway's formalism, it's convenient to envision a strategy in a logically equivalent but conceptually distinct way: you prove through (Conway) induction that a certain set of positions is winning for a given player, by showing that they can play so that the next player is forced to move to one of the positions you've already proved is winning.

In your tic-tac-toe example, you could prove that "every position which consists of pairs of reflected pieces, plus an extra piece, is drawing for the player in turn, by moving to the position which adds the reflection of the extra piece". This sidesteps having to define a strategy at all!

[Violeta Hernández]

Yves Jäckle said:

Violeta Hernández said:

Here's a proof of concept of my idea: https://github.com/leanprover-community/mathlib4/compare/master...vi.concreteGame

I'm happy to see you're working on the subject too !

I'm pretty much the maintainer of the SetTheory folder, feel free to ask anything :stuck_out_tongue:

[Yves Jäckle]

I have a workshop at 12 today, so I have to get going, but I'll get back to this :+1:

[Daniel Weber]

Related thread

[Yves Jäckle]

Some thoughts:

• Violeta Hernández said:

Here's a proof of concept of my idea: https://github.com/leanprover-community/mathlib4/compare/master...vi.concreteGame

I really like this formalism. I suppose one can express tic-tac-toe in it by letting alpha be Fin D -> Fin n -> Fin 3 (gridpoints of the d-dimensional cube of length n, in a state of being either unclaimed, or claimed by the first or second player). Then The "subsequent" relation would be that there exists a point that has changed from being unclaimed to claimed, in the case that there are unclaimed points left, and no combinatorial line was fully colored.

• How would you fit the notion of a draw into Conway's formalism ? From what I understand the game is win-lose only, where a player loses if their type is empty. A speaking of this, wrt:
  Violeta Hernández said:

We at some point had definitions like PGame.Winning, PGame.Losing, etc. which determined whether a game could be won or lost by a given player. I refactored them out since they were nothing more than x > 0, x < 0, etc. But if they're helpful in removing a layer of abstraction we could bring them back as abbrevs or something.

Is my above understanding even correct ?

• Wrt:
  Violeta Hernández said:

The usual way to envision a strategy is "if a player always replies to a game state with a given move, they will preserve some invariant, which implies they will never run out of moves, which implies they win". I think that in order to work with Conway's formalism, it's convenient to envision a strategy in a logically equivalent but conceptually distinct way: you prove through (Conway) induction that a certain set of positions is winning for a given player, by showing that they can play so that the next player is forced to move to one of the positions you've already proved is winning.

In your tic-tac-toe example, you could prove that "every position which consists of pairs of reflected pieces, plus an extra piece, is drawing for the player in turn, by moving to the position which adds the reflection of the extra piece". This sidesteps having to define a strategy at all!

This sounds like a good approach. The invariant for tic-tac-toe would be that "for all pairs, if one point of the pair is claimed, then the other is claimed by the other player or isn't claimed".

• Have you thought about strategy stealing for Chomp in Conway's formalism ?

[Yves Jäckle]

Daniel Weber said:

Related thread

This is very interesting ! Though the fact that in your GeneralGame and in the Nash-equlibria-game-theory, players act simultaneously changes almost everything when compared to the turn-based context. I'm not aware of formal connections between these two types of game theories.

[Yves Jäckle]

Violeta Hernández said:

I'm pretty much the maintainer of the SetTheory folder, feel free to ask anything :P

Maybe its a good idea to have one big online meeting with all people interested ?

[Michael Rothgang]

One by-stander comment: if I were programming, I'd make a custom enum (i.e., inductive in Lean with constructors claimedA, claimedB, unclaimed or similar). That type is finite (and in bijection to Fin 3), so your proofs work the same - right?

[Yves Jäckle]

@Violeta Hernández The ideas you stated above and in your branch may allow to make the connection between formalisms. I was thinking of:

import Mathlib.SetTheory.Game.Basic

open SetTheory

partial def PGame_Preds (hist : List β) (win? : List β → Prop) [DecidablePred win?] (legal : List β → (β → Prop)) : PGame :=
  if win? hist
  then (0 : PGame)
  else PGame.mk {act : β // legal hist act} {act : β // legal hist act} (fun act => PGame_Preds (act.val :: hist) win? legal) (fun act => PGame_Preds (act.val :: hist) win? legal)

termination may require well foundedness of the relation of a history extending another by one action, where the extention is legal and neutral (doesn't satisfy the winning predicate). We would have to assume this, and that seems similar to what's going on in my "ConwayInduction.lean" file.
Anyway, off to bed.

[Violeta Hernández]

Various @Yves Jäckle replies:

Yeah, TicTacToe = Fin D → Fin n → Fin 3 (or something equivalent) would suffice to represent tic tac toe. Though this would also include some illegal states like, two X and zero O, but maybe we don't care about that. Left and right subsequency can be defined exactly as you say. To prove subsequency is well-founded, simply notice that any move by any player decreases the number of empty spaces.

Draws don't really exist within Conway's formalism. At the end of each game, exactly one of the two players will win. You'd instead have to work with draws indirectly. For instance, to prove the left player always has a drawing strategy, you can add a special "draw" game state and declare that it's subsequent for the left player to any drawing state, but that nothing is subsequent to it. So in this modified game, what you want to prove is that the first player has a winning strategy - if they can guarantee to either win or draw in tic tac toe, then either they win in this modified game, or they first draw in tic tac toe, which gives them a move in modified tic tac toe to the "draw" state, which is a losing state.

To prove strategy stealing in the poset game within Conway's formalism, suppose that the game is won by the second player. Then {⊤}ᶜ must be a winning position, and there exists some next move s which is losing. Show that in fact, it was possible to move to s from the initial position, giving a winning strategy to the first player. This is a contradiction, so actually the game is won by the first player.

[Violeta Hernández]

Yves Jäckle said:

Violeta Hernández The ideas you stated above and in your branch may allow to make the connection between formalisms.

I don't quite understand your code snippet. What do hist, win?, etc. represent here?

[Yves Jäckle]

Violeta Hernández said:

I don't quite understand your code snippet. What do hist, win?, etc. represent here?

So the way I modeled games is by considering a list of the actions played by the players so far, List β, and using predicates to decide if the game is won by a player or is a draw, and to decide if a next action is legal wrt. the previously played once (hence, the state of the game so far). Strategies end up being functions mapping histories of previous moves to the next move to play.
I think that above code snippet, or something more elaborate but in the same direction, could be the equivalent PGame representing this game.

[Yves Jäckle]

Well, it looks like the Conway formalism is quite capable after all !
I'll withdraw from trying to get my stuff into mathlib :+1:

[Niels Voss]

Yeah, TicTacToe = Fin D → Fin n → Fin 3 (or something equivalent) would suffice to represent tic tac toe. Though this would also include some illegal states like, two X and zero O, but maybe we don't care about that. Left and right subsequency can be defined exactly as you say. To prove subsequency is well-founded, simply notice that any move by any player decreases the number of empty spaces.

I was going to suggest looking at Chapter 22 of Volume 3 of Winning Ways for Your Mathematical Plays, where Tic-Tac-Toe was analyzed, but it seems to just be a brute-force analysis and doesn't really take advantage of the Conway formulation.

I haven't had time to read it, but fortunately, it does seem to analyze some generalizations of Tic-Tac-Toe that might be of interest.

[Niels Voss]

I looked at both Sven Manthe and Yves Jäckle's formulations some time ago, and my impression was that they both used a data structure that looked somewhat similar to https://en.wikipedia.org/wiki/Tree_(descriptive_set_theory)

Maybe it might be worth trying to get a theory of DSTTrees into Mathlib first? Just a suggestion though

[Michael Rothgang]

#18763 defines DSTTrees and is waiting for review. I heard much more theory has been developed in a separate repository.

[Violeta Hernández]

Yves Jäckle said:

So the way I modeled games is by considering a list of the actions played by the players so far, List β, and using predicates to decide if the game is won by a player or is a draw, and to decide if a next action is legal wrt. the previously played once (hence, the state of the game so far).

Encoding the state of a game as its entire history is redundant for most games. For games where the history of plays is relevant, you can simply make said history the game state. In any case, you don't need to work directly with List B.

[Violeta Hernández]

Niels Voss said:

I looked at both Sven Manthe and Yves Jäckle's formulations some time ago, and my impression was that they both used a data structure that looked somewhat similar to https://en.wikipedia.org/wiki/Tree_(descriptive_set_theory)

Maybe it might be worth trying to get a theory of DSTTrees into Mathlib first? Just a suggestion though

PGame already serves essentially that same purpose.

[Violeta Hernández]

One can think of a PGame as a tree with two-colored branches (representing which player can perform which move) and no infinite paths

[Violeta Hernández]

Borel determinacy requires a different data structure because it talks about a different type of game, with infinite length

[Niels Voss]

My impression was that PGame was that it was kind of like PSet except instead of defining sets, you defined "double sets". Are there tools to make defining PGames easier, like being able to convert a pair of well-founded relations into a PGame?

[Violeta Hernández]

We have little API for constructing explicit PGames. There's docs#SetTheory.PGame.ofLists and I think that's it

[Violeta Hernández]

And of course, we really should have done something like ofSets instead.

[Violeta Hernández]

The thing about well founded relations you mention is basically my ConcreteGame idea from earlier. Note that you actually need a slightly stronger condition: the "either of" relation of both relations is well-founded

[Niels Voss]

To make sure I understand properly, the advantage of using PGame over ConcreteGame is that you can add games and treat them as a homogeneous class, right (kind of like the advantage of using ZFSet over Type)?

[Violeta Hernández]

What do you mean by homogeneous class?

ConcreteGame isn't meant to be a replacement for PGame, but rather a convenient tool for constructing them

[Niels Voss]

If we were to formulate only a single type of game, like Chess, it would make more sense to define the type ChessPos of chess positions and just use well founded relations on it, instead of constructing a term in PGame. But if you wanted to add different types of games together, then PGame might make more sense.

[Niels Voss]

Or that's my current understanding at least

[Violeta Hernández]

My ConcreteGame class allows you to take a term in ChessPos and turn it into a PGame, which then allows you to talk about winners, losers, and all that good stuff

[Violeta Hernández]

Of course you're still doing most of the logic within ChessPos, the PGame conversion is mostly just there to state the results