What's the current state of Surreal Numbers in Lean/Mathlib?

Stream: new members

[Dan Abramov]

I've started reading a bit more about them and was wondering if Lean has some support for them.

I've seen a thread from a few years ago about them but not sure what the latest status is. I see there's some stuff on them in Mathlib. How extensive is it? I'm a noob so I wouldn't be able to tell — I guess I'm trying to figure out if it's in a "just a stub" phase, or "just the most important definitions", or "all related definitions and some results", or something in between.

Thanks!

[Aaron Liu]

See https://github.com/vihdzp/combinatorial-games

[Dan Abramov]

Ahh fantastic! Thanks

[Aaron Liu]

#announce > Combinatorial game theory repository < This is the announcement

[Dan Abramov]

Not sure if I'm reading too much into it or if Conway is essentially describing inductive types here..

Screenshot 2025-07-11 at 22.03.52.png

[Aaron Liu]

Dan Abramov said:

Not sure if I'm reading too much into it or if Conway is essentially describing inductive types here..

Screenshot 2025-07-11 at 22.03.52.png

that's exactly how I interpreted it lol

[Aaron Liu]

he's doing quotients of inductive types

[Kevin Buzzard]

Or possibly higher inductive types