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. On December 8, 2021 8:04:41 AM PST, "David A. Wheeler" <[email protected]> wrote: >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 > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/387AEE25-86DC-4E0C-993A-DFD9CC09C94C%40panix.com.
