Board Games in Lean

Stream: new members

[Harrison Boorstein]

Hi! I'm new to Zulip and was encouraged to discuss my project here. My background is in mathematics (homological algebra), but I've been enjoying working on applications of Lean outside math. I modeled the board game Clue in Lean as a demonstration. For any interested, the formalization is here: https://github.com/hhboorstein/ClueLean. Included is both the codified ruleset, entity types, and a gameplay ledger with deductions (I lost the game by one turn :sweat_smile:).

I'm left with two lingering thoughts that I hope the community could nudge me on:

1. What board game should I work on next? I'm enjoying these capsule projects that force me to stretch beyond mathematics. The goal is to work toward projects with serious business applications. I'm inspired, e.g., by the Lean implementation of Cedar.
2. In writing a project without Mathlib, I sorely missed my beloved apply at tactic. Appreciating that there are roadmap considerations for core Lean, how could I start exploring contributing this tactic to either the core library or batteries? Is this a normal request? I've read through the contribution guidelines as a start, and I certainly would take this project slowly and deliberately, likely pairing with someone more experienced in metaprogramming.

Excited to be part of the community!

[Ruben Van de Velde]

Probably for a small tactic like that, you could also copy it into your project

[Harrison Boorstein]

Ah so true, definitely the right place to start Ruben, thank you!

[Robin Arnez]

Also, the mathlib-free alternative of apply at is replace h := my_lemma h if you're curious

[Mirek Olšák]

Regarding what other games could be interesting, Hex is a mathematically nice game. And projex is mathematically even crazier.

[Harrison Boorstein]

@Mirek Olšák Woah Hex has far more topology going on than I anticipated! What we’re you thinking with respect to implementing it in Lean? Would the goal be to prove something like: Given the current state, player $i$ could guarantee a win with both players playing perfectly? Like deductions about the solution space, or theorems around the topology of the game itself?

[Mr Proof]

Hello. This is right up my alley!
I have been making a puzzle solver also, not in Lean, but I am finding that I might want to integrate Lean into it at some point or at least learn from it in order to do general goal proliferation and such like.

Suggestions for board games: Take a look at "General Game Playing at Stanford" which was a competition to make a general game playing agent. It has lots of simple board games and puzzles which you might try. That is if your aim is to try and write an AI solver(?)

Can you say more about how your project works?

I can see two main ways to encode games in Lean. My preference would be to encode the game states as dependent types. e.g. a tic-tac-toe board might be State(1,0,0,-1,0,1,1,1,-1):Type . And then a move to place an X in top right would be of type:

MoveXTR : ForAll a b c d e f g h , State(a,b,0,c,d,e,f,g,h)->State(a,b,1,c,d,e,f,g,h)

Composing the different moves together would be a game and then you might need some type equality between the final state and the win-condition. An AI which solved the game would then by a tactic e.g.

Exists a b c d e f g h i : State(a,b,c,d,e,f,g,h,i) and ((a=1 and b=1 and c=1) or ....) :=by MyTicTacToeTactic

But this would only prove such a win was possible not that it is the best win using minimax etc. Well that would be the pure mathematical way of doing things I think but maybe not the best if you just want to make a fun game playing program.

These are just some food for thought. Good luck. :slight_smile:

[Mirek Olšák]

What could be done with Hex:

• Some time ago, I played with interactively proving hex puzzles (just in Python, but should be doable in Lean too): https://github.com/mirefek/HexProver, the idea is that to prove you always win, you must either decompose opponent moves into regions, and provide a winning move for each region, or decompose the game into two separate smaller subgames that you can win both. In the prover I made, one subgame is ensuring a specific connection, and the other one, assuming this connection is solid, winning the rest of the game.
• A little more high level logic, say Ladders
• Proving the global topological theorems, such as exactly one player can make a connection. Or that on a board n x (n+1), the player connecting the shorter distance has a winning strategy, even if he starts second.

[Harrison Boorstein]

Thanks @Mr Proof ! This project was focused on deriving the solution to a single play through of a hidden information game, so I like the idea of next stretching to work on a game solver in generality.

[Harrison Boorstein]

@Mirek Olšák Cool, I like how this requires connecting local and global results about the game state. I gotta read more of that wiki :nerd:

[Violeta Hernández]

We have an entire library dedicated to combinatorial games, btw: CGT#IGame

[Violeta Hernández]

We don't yet have much about actual games, to be honest. We've mostly focused on the algebraic theories of surreals and nimbers. But contributions would be very welcome!

[Violeta Hernández]

(In particular, the question of how to encode game states already has an answer: CGT#GameGraph)

[Violeta Hernández]

We also have a channel for discussion on combinatorial games: #combinatorial-games

[Mirek Olšák]

Combinatorial games do not cover potentially infinite games, right? (like Chess, or Gomoku)

[Aaron Liu]

we also have CGT#LGame

[Snir Broshi]

They don't cover Clue, which is what started this thread

[Violeta Hernández]

Yeah, we don't really have anything about games of partial information. But Hex (which was mentioned in this thread as well) does fall under our jurisdiction.

[Mirek Olšák]

Yes, I agree Hex is a nice terminating game. I don't see much of use of CGT for Hex -- you don't really decompose Hex in the sense CGT does. I can imagine arguing that a certain move is strictly better than another using CGT (but that is a bit more high level).

[Violeta Hernández]

The theorems that Hex is never drawn, and that the first player (non-constructively) has a winning strategy, would definitely belong in our repository.

[Violeta Hernández]

If nothing else, IGame is useful here as a canonical way to define the game mathematically, and to talk about its outcome.

[Harrison Boorstein]

Violeta Hernández said:

(In particular, the question of how to encode game states already has an answer: CGT#GameGraph)

Oh cool, it’s interesting to see where my ideas for recording gameplay match up and diverge from this!

[Harrison Boorstein]

Fascinating how much of the structure is derived from GameFunctor

[Violeta Hernández]

Yep, it turns out well-founded games and loopy games are just inductive/coinductive variants of the same underlying functor.

[Harrison Boorstein]

That’s rad, I wanna dig into this repo more. I’ve been largely focused on modeling games of deduction/partial information. I wonder if my next foray should be one with perfect information instead?? :thinking:

[Kevin Buzzard]

If you're going to prove that a unique player wins hex then you may as well prove the Jordan Curve theorem, which would surely be welcome in mathlib.

[Mirek Olšák]

Oh, Mathlib doesn't have it yet? Just for Hex, doing combinatorial topology should be easier than real topology (no fractal-like shapes). However, if one would like to generalise the results to planar graphs, a theorem for handling them would be needed.

[Kevin Buzzard]

My understanding is that when people formalize JCT they often first reduce to a combinatorial statement.

[Snir Broshi]

The formalization of JCT first reduces the problem to a polygonal path with edges parallel to the axes, then reduces to the fact that K33 is nonplanar

[Snir Broshi]

btw here's a recent discussion about JCT where it seems they are closing in on it hopefully

[Violeta Hernández]

To be fair, you don't need JCT to define the game of hex. The game has a finite amount of possible moves, so it must eventually end, and normal game convention dictates that a player without moves loses.

Of course, the theorem that any position without moves must be one where a player has connected a path from one side of the board to another would require JCT.

[Violeta Hernández]

Its strategy stealing argument is also one can be generalized to other games. It should at the very least work for any game where players add pieces, and where having more pieces is always an improvement of your position (tic tac toe is an important example here). There might be an even more abstract formulation, akin to the theorem CGT#IGame.Impartial.fuzzy_zero_of_forall_exists we have for impartial games.

[Kevin Buzzard]

Hex is not played under the normal game convention. A game of Hex stops when one player makes a chain, not when the board is full.

[Violeta Hernández]

You can transfer it to a normal play convention, by declaring that a position where a chain exists has no moves for either player.

[Mirek Olšák]

Sure, the strategy stealing argument is pure CGT, on the other hand "no draws", "no double wins", and "strategy for n x n+1" are mostly topology arguments without CGT theory.

[Violeta Hernández]

I think we can still welcome them in our repository, as long as the brunt of the topological work stays within Mathlib.

[Harrison Boorstein]

Kevin Buzzard said:

If you're going to prove that a unique player wins hex then you may as well prove the Jordan Curve theorem, which would surely be welcome in mathlib.

Sounds like a good project, thanks, I’d love to take a stab at it! Any suggestions on channels to discuss progress/pairing on a solution?

[Snir Broshi]

Hold up; do you mean you're taking a stab at proving the JCT?

[Harrison Boorstein]

Are we not talking about this? Hasn’t this been known for almost 150 years?

[Snir Broshi]

Yes we are

[Violeta Hernández]

i think the JCT is one of those things we could have proved ages ago, but we choose not to because we can't yet do it "correctly"

[Snir Broshi]

If you want to work on it then probably discuss it on the thread I linked above, and I think specifically tag Sébastien Gouëzel since I think they know what's up with JCT

[Snir Broshi]

Sébastien said they think we'll finish JCT this year

[Snir Broshi]

I think it's a bit daunting to jump from formalizing a board game to the depths of algebraic geometry (I think?), but if you're proficient in algebraic geometry then go for it

[Harrison Boorstein]

Is the deficit insuffient machinery from homology in Lean?

[Harrison Boorstein]

I worked in homologica algebra for a time, so I thought initially that adding JCT to Lean was just a matter of filling in a gap that no one had gotten around to. I get the impression now that there’s more work that needs to be done to get Mathlib to a state to properly prove JCT.

[Snir Broshi]

Do you know what that work is? (I'm very interested in JCT but pretty clueless about homology)

[Harrison Boorstein]

@Snir Broshi I’ll read through that thread you linked and try to get a handle on what remains… :saluting_face:

[Kevin Buzzard]

Mathlib isn't just about formalising proofs. It's about formalising the right proofs, which sometimes involves work that is not at all beginner-friendly.

[Ruben Van de Velde]

That said, if you want to prove something mainly to learn more lean, and not to extend mathlib, that's fine too!

[Mirek Olšák]

Snir Broshi said:

I think it's a bit daunting to jump from formalizing a board game to the depths of algebraic geometry (I think?), but if you're proficient in algebraic geometry then go for it

Algebraic geometry? I thought it is actually closer to algebra...

Harrison Boorstein said:

Snir Broshi I’ll read through that thread you linked and try to get a handle on what remains… :saluting_face:

You could also assume it is already proven, and try to build something on top of it. If the status is it should be proven soon, perhaps someone already even has a proof but not good enough for mathlib. Reading the thread, and asking relevant people indeed sounds like a good strategy.

[Snir Broshi]

There's an open PR about polygons that assumes JCT I think, so the statement should be in Mathlib soon