Thank you all! It's great to meet you. I'll probably start setting up the github process over the next few days, so thank you for the instructions, Glauco! I'll reply to this thread if there's something I don't understand.
Thanks for the recommendation, Jim! It might be a bit incomprehensible to me for now but I'll look back on it after I have a bit more experience. I've been thinking about learning some type theory (and category theory, for that matter), so I wouldn't mind diving into that book and hoping I can make sense of it. I also didn't know about the issues page - I'll probably start with reproving some existing theorems but at some point I'll definitely look through the list of issues and see if there's something doable. I might take a while to familiarize myself enough with working in Metamath to actually be able to do anything, but once I feel comfortable with the tools I'd love to help you, Scott. The Gonshor book looks super interesting in any case, so I'll probably read it after Knuth. - Noam On Mon, Jan 13, 2025 at 3:27 PM Scott Fenton <[email protected]> wrote: > Hi Noam, > > Great to see you! We always welcome new contributors. If you want to get > into surreal work, I'm mostly working off On Numbers and Games by Conway > and An Introduction to the Theory of Surreal Numbers by Gonshor. The next > step there is actually a mix of set theory and arithmetic. There is a > second type of addition defined on ordinal numbers called "natural > addition". It gives the same results over the natural numbers but it > differs at _om and above. The next couple of proofs in the surreal numbers > depend on induction on the natural sum of the birthdays of various > surreals. I'd appreciate any help I could get there. > > -Scott > > On Sun, Jan 12, 2025 at 10:47 AM Noam Pasman <[email protected]> > wrote: > >> Happy New Year! >> >> I'm an undergraduate right now, and I spent much of last year reading >> through most of Parts 1 through 4 of the Metamath Theorem List. I'm hoping >> to do some more set theory in the future, but there aren't any mathematical >> set theorists at my college so I don't really know where to continue from >> what's in Metamath. I'm planning to read some of the set theory books >> referenced in the Theorem List, particularly either Takeuti and Zaring's >> *Introduction >> to Axiomatic Set Theory* or Suppes's *Axiomatic Set Theory*, but I would >> appreciate some advice on which of these (and/or some other book(s)) is >> most helpful. I'm also currently in the process of applying to REUs, and I >> haven't found any for set theory but if there are some I'm not aware of (or >> generally any way to do set theory as an undergraduate) I'd love to hear >> about them. >> >> I'm also hoping to contribute to set.mm, and I read the two github pages >> on contributing but I wanted to ask about who I should contact in case I >> have a problem with setting everything up. Eventually, I'd love to help >> with some project in the database if needed and if I already somewhat >> understand the concepts. I've been reading Knuth's *Surreal Numbers* and >> I saw that work has begun on moving theorems on surreal numbers from >> Mathboxes to main, so I'd love to give any help I can towards developing >> that further (obviously after reading much more material on the subject). >> If there's another project that I'd be more useful for, that's good too! >> >> - Noam Pasman >> >> -- >> 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 visit >> https://groups.google.com/d/msgid/metamath/CABJcXbRF5BsRyNC_hf3L_EmhmuSvfdaN3EKy%2BFOs10DLRUjPOg%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CABJcXbRF5BsRyNC_hf3L_EmhmuSvfdaN3EKy%2BFOs10DLRUjPOg%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > 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 visit > https://groups.google.com/d/msgid/metamath/CACKrHR-d%3DC7UHPvZZq0wYru0nzUF0PiZsZ-u8WbDrv0xCAmVFg%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CACKrHR-d%3DC7UHPvZZq0wYru0nzUF0PiZsZ-u8WbDrv0xCAmVFg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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 visit https://groups.google.com/d/msgid/metamath/CABJcXbQqhasoYyEi8tX_zZycDrhRgHU-OVF9LC-8_FSu%2BB7P-A%40mail.gmail.com.
