Hi, I've been having a few issues with setting everything up. I was able to fork, clone, and branch the repository, but I don't know how to actually open up the set.mm file and add a mathbox there. I downloaded mmj2 in the hope of opening set.mm from there, but when I followed the QuickStart instructions I got the following error:
Processing RunParmFile Command #1 = LoadFile,set.mm Java heap space java.lang.OutOfMemoryError: Java heap space Am I doing this in the wrong way? Or do I just need to find a way to allocate more memory to mmj2? Thanks, Noam On Mon, Jan 13, 2025 at 10:43 PM Noam Pasman <[email protected]> wrote: > 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/CABJcXbSvK8FjiiHqg1RP8NL4tbLkqAhiVZtP291cd7xGSJZ2ww%40mail.gmail.com.
