Congrats to Scott Fenton on surreal work

[David A. Wheeler]

All:

I wanted to publicly congratulate Scott Fenton on his work
to formalize surreals. The merged pull request is here:
https://github.com/metamath/set.mm/pull/2360

He defined surreals in Metamath 10 years ago, but now
we have a Metamath formalization of their fundamental theorem.

Especially interesting to me when I commented about it, he said,
"It literally took a new proof coming out in the literature for
it to get formal enough for Metamath!". I'm pretty sure he meant
[Lipparini] Lipparini, Paolo,
<I>A clean way to separate sets of surreals</I> arXiv:1712.03500 (20-May-2018);
available at <A HREF="https://arxiv.org/abs/1712.03500">
https://arxiv.org/abs/1712.03500</A> (retrieved 7 Dec 2021).

I think that comment is telling. Significant parts of set.mm necessarily formalizes
"relatively old well-known mathematics". Here's a case where we're
formalizing recent work. I know it's not the only case, but I find
that encouraging.

--- David A. Wheeler

[Jim Kingdon]

Oooh, awesome. For those who haven't been following, the result is "given two sets of surreals such that one comes completely before the other, there is a surreal lying strictly between the two. Furthermore, there is an upper bound on the birthday of that surreal." My mental model of the surreals had been "the real numbers glued to the ordinals" but clearly I need to amend that with "yeah, but dense all the way" or something of the sort.

And agreed about it being cool to formalize new mathematics. Anyone want to take a crack at proving in iset.mm that the Schroeder-Bernstein theorem implies excluded middle (full excluded middle, not just a weaker omniscience principle)? I've looked over the 2019 paper which proves it but I think formalizing this might be beyond my abilities.

Seeing that people were using provers to discover new theorems in type theory and then only later writing them up informally in the HoTT Book was another example of me being inspired about provers potential to be in the thick of mathematics, not just a curiosity on the side.

[Scott Fenton]

Thanks for the compliments!

To fully examine density in surreals, also take a look at ~ nodense and ~ nocvxmin .  They give that there's a unique birthday-minimal element of any convex class of surreals. To recover Conway's simplicity theorem (the uniqueness of the surreal cut) you need to combine those theorems with ~ noeta .  I'm actually working on that today.

As a side note, does anyone know any good references on recursion over weakly founded relationships (that is, where R Fr A as opposed to R We A)? I'm going to need that for the next step in surreals - defining addition and multiplication.

-Scott

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/387AEE25-86DC-4E0C-993A-DFD9CC09C94C%40panix.com.