Violeta Hernández Palacios: A Nimble Introduction to Nimbers

Stream: Lean Together 2025

[Jireh Loreaux]

Discussion thread for this talk.

[Junyan Xu]

Regarding multiplication on games: #maths > Well-founded recursion for pgames @ 💬

[Violeta Hernández]

Here's my slides:
main.pdf

[Violeta Hernández]

re the state of CGT on Mathlib: one of the main blockers so far has been that our current definition docs#SetTheory.PGame is wrong... or at least, doesn't have the correct notion of equality. Two games are only equal when not only the indexing functions for left and right games are equal, but the indexing types are as well. This is much stronger than the notion of equality that you would get by formalizing games from a set-theoretic standpoint.

[Violeta Hernández]

But there's currently some open PRs towards defining IGame or "games up to identity" which should be the correct quotient.

[Kevin Buzzard]

Random idea: define the product of two (short?) games to be the following game: a move in the product game G x H is a move in one or both of G and H. Presumably this doesn't work because it would have been noticed by now.

[Violeta Hernández]

That doesn't work, it would give 2 × 2 = {2 × 1, 1 × 2, 1 × 1 | } = 3

[Kevin Buzzard]

I thought that this was correct? Did I misread your slides?

[Violeta Hernández]

Oh wait, you mean for nimbers rather than combinatorial games

[Kevin Buzzard]

(but I don't expect it to work)

[Kevin Buzzard]

yes that's why I posted it in the nimber thread :-)

[Kevin Buzzard]

but I'd never seen this multiplication before so my intuition is way off at this point

[Violeta Hernández]

You can use the Sprague-Grundy algorithm to find the nim value of the impartial game you describe, at least for small values. I could try coding something up and see what happens

[Violeta Hernández]

At worst, we get a potentially interesting setup for a math olympiad problem :stuck_out_tongue:

[Violeta Hernández]

Well we clearly don't get nimber multiplication

[Violeta Hernández]

Your operation would satisfy 0 * x = x for any x

[Junyan Xu]

You can do transfinite nimber multiplication (below omega^omega^omega) in CGSuite since version 2.1:

Introduces a few new features, including scatterplots for integer sequences (such as nim value sequences) and support for the Conway-Lenstra theory of transfinite nim arithmetic. Also includes various bugfixes, including several UI fixes for Windows installations.

Slightly more details are found in the repo.

[Violeta Hernández]

Huh really? I was under the impression that the theory was only mostly solved

[Junyan Xu]

The algorithm depends on Lenstra's constants to work efficiently, I think, which are computable but each one depends on the previous ones, and the current record is p=173 (Figure 4.1, Chapter VIII of Siegel's CGT book). I think some value(s) don't agree with my computation and may be wrong, probably the last one. (Edit: there are more values here and here and I don't find any disagreement with my computation now.)
The code to compute those constants

[Violeta Hernández]

Violeta Hernández said:

Well we clearly don't get nimber multiplication

I think we should get natural addition, aka docs#Ordinal.nadd, aka game addition for ordinals rather than for nimbers

[Violeta Hernández]

Haven't managed to prove it (formally or informally) yet

[Junyan Xu]

Section 3 of Lenstra's paper Nim multiplication discusses a more playable version of the games corresponding to product of nimbers:
image.png

[Violeta Hernández]

By the way, I'm not being able to install CG Suite. Any idea what this is about?
image.png

[Junyan Xu]

I've been able to install latest version 2.1.1. Haven't seen this error before.
image.png

[Junyan Xu]

There's a CGT Discord server with a cgsuite channel in it: https://discord.gg/9AkcAwBqTF
You'll see the author there and you can also type into the channel to get expressions evaluated.

[Mauricio Collares]

Wrong Java Runtime version, perhaps?

[Violeta Hernández]

Junyan Xu said:

You can do transfinite nimber multiplication (below omega^omega^omega) in CGSuite since version 2.1

Oh, I see what my misconception was. I saw Lenstra giving a table of the first few values for some nimbers important to nim multiplication, but I thought that was "state of the art progress" rather than "specific values from an algorithm"

[Violeta Hernández]

Worth pointing out that an algorithm for the transfinite nimber inverse is still (afaik) not known

[Kim Morrison]

Violeta Hernández said:

re the state of CGT on Mathlib: one of the main blockers so far has been that our current definition docs#SetTheory.PGame is wrong... or at least, doesn't have the correct notion of equality. Two games are only equal when not only the indexing functions for left and right games are equal, but the indexing types are as well. This is much stronger than the notion of equality that you would get by formalizing games from a set-theoretic standpoint.

@Violeta Hernández, I think this is an inappropriate characterization of the intent of this formalization. The docs are quite clear that combinatorial games are Game, not PGame, and PGame is not intended to have the right equality -- it's where we set up the equivalence relation to define Game.

Moreover, I've been surprised at the criticism about the Relabelling data type, when still no one has attempted to set up the basic theory of dominated and reversible positions, where (I suspect; this hasn't been done) it will be useful. If you pass to the type with the correct equality too quickly, you'll only add the suffering in situations where you really need to reason about indexing types.

[Violeta Hernández]

Game is an important quotient, but it's not what one envisions as a "concrete game". Most crucially, there's no way to consistently talk about the left and right set of a Game, the same way we can with PGame and could with IGame.

Maybe this isn't the issue singlehandedly impeding progress on combinatorial games, but at least for me, this and other refactors at the level of PGame (which I do believe to have important long-term benefits) have been what's taken my attention.

[Violeta Hernández]

I'm not familiar with dominated and reversible positions. How would Relabelling be useful in talking about them?

[Junyan Xu]

Dominated and reversible options are discussed in Section II.2 (Canonical Form) of Siegel's book, and I think @Tristan Figueroa-Reid is trying to develop some theory about them: #maths > What to do about PGame @ 💬

[Junyan Xu]

Worth pointing out that an algorithm for the transfinite nimber inverse is still (afaik) not known

The inverse is at least computable in the algebraic closure of 2 (i.e. below omega^omega^omega); every element has finite order there so you can keep multiplying and take the value right before you get 1.

[Violeta Hernández]

Awesome! So this is not quite "this isn't known" but rather "I don't know it" :stuck_out_tongue:

[Violeta Hernández]

But it also means we could have formally-verified nimber arithmetic below ω^ω^ω as a formalization goal

[Violeta Hernández]

Violeta Hernández said:

I'm not familiar with dominated and reversible positions. How would Relabelling be useful in talking about them?

Read a bit about this. I really don't see how Relabelling is in any way relevant. All we need is some function to remove an option from a game (which iirc is an open PR) and some predicates on whether a given position is dominated/reversible.

[Tristan Figueroa-Reid]

Violeta Hernández said:

I'm not familiar with dominated and reversible positions. How would Relabelling be useful in talking about them?

Relabelling would not be relevant for talking about dominated and reversible positions.

[Tristan Figueroa-Reid]

An IGame would be much more useful for that, as we can say that if two games are equivalent, then their undominated and unreversed selves must be identical.

[Violeta Hernández]

Sorry, I'm just now realizing we're still in my nimbers thread. If there's any more discussion on this we can move it to the main CGT discussion thread.

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/9eI3eI7YssE