search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 298 forks source link

Expand the surreals library #1046

Open rwbarton opened 5 years ago

rwbarton commented 5 years ago

We currently have a definition of the surreal numbers in surreal.lean, but there is still more to be done here. The next steps would be to show that the arithmetic operations defined on pSurreal descend to the surreals and make the surreals into a field.

kim-em commented 5 years ago

An ANU student is developing the theory of combinatorial games. This will build off the beginning of the current surreal file (ordering, negation, addition), but does not go in the direction that Reid indicated above (arithmetic on surreal itself).

kim-em commented 5 years ago

The first batch of work on combinatorial games, by Isabel Longbottom, Reid, and myself has landed in mathlib as https://github.com/leanprover-community/mathlib/commit/b41277c70937d8cd46639bbef674e656e8e397dd. This was mostly about games, rather than surreals, but it has pushed things along to proving add_semigroup surreal.

vihdzp commented 2 years ago

As I've mentioned to what feels as everyone in Zulip, I've done a large amount of progress proving that surreal multiplication is well-defined. Currently there's a bunch of large PRs that are blocking my progress, but I think that in approx 1 month I should have the proof produced.