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/086AC9D3-2576-4386-8306-80F6F5DB9966%40dwheeler.com.
