Misère play

Stream: combinatorial-games

[Violeta Hernández]

@Tomasz Maciosowski Hi! We have our own channel now.

[Violeta Hernández]

I've kept thinking about how to implement this in Lean. I do think my idea of using toMisere is useful if as nothing else than an auxiliary definition. It gives us all of this outcome machinery basically for free, and in particular it allows us to state very simple definitions of MisereEQ and MisereLE.

[Violeta Hernández]

I'd pretty interested in the triviality theorem you mention, x =m Any game 0 <-> x = 0. I imagine this generalizes to x =m AnyGame y <-> x = y. Is there a proof of that somewhere?

[Tomasz Maciosowski]

Hi! Sorry I'll be a bit slow cause I have a bit on my mind for the next week but I'll be looking into this for sure. I'd like to spend some time playing with your definition to see how easy I can translate some of the proofs

[Tomasz Maciosowski]

Violeta Hernández said:

I'd pretty interested in the triviality theorem you mention, x =m Any game 0 <-> x = 0. I imagine this generalizes to x =m AnyGame y <-> x = y. Is there a proof of that somewhere?

That doesn't hold iirc they're still equivalence classes but much smaller. Let me look for some reference

[Tomasz Maciosowski]

Misère canonical forms of partizan games [p. 9] is a good one I think, the bound on number of misere games born by day 3 is under $2^{512}$ so there are some different game forms that are equal in misere

[Tomasz Maciosowski]

Just randomly bumped into it, Simplification of Partizan Games in Misère Play has actual example
Screenshot_20250729_001142.png

[Violeta Hernández]

Ooh, that'd be good for the counterexample folder!

[Violeta Hernández]

Tomasz Maciosowski said:

Hi! Sorry I'll be a bit slow cause I have a bit on my mind for the next week but I'll be looking into this for sure. I'd like to spend some time playing with your definition to see how easy I can translate some of the proofs

If you don't mind, I could try adapting your PR myself.

[Violeta Hernández]

(deleted)

[Tomasz Maciosowski]

Sure, go ahead! I'll have way more time next week to play with lean