Questions on doing more Set Theory and Metamath

[Noam Pasman]

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

[Glauco]

Hi Noam, and welcome to the Metamath community!

Regarding contributing to set.mm, there are several amazing maintainers who can provide guidance far beyond what I can offer here. That said, here’s a general outline to help you get started:

1. Fork the set.mm repository: This creates your own copy to work on.
2. Clone your fork locally: Use git clone to download your forked repository to your machine.
3. Create a branch: Set up a dedicated branch for your new mathbox.
4. Add your mathbox: Insert an empty mathbox into set.mm following the conventions used by other contributors.
5. Start with a simple theorem: Add a small theorem to your mathbox. A good example could be a variation of an existing theorem from the main section, where a $d condition is replaced with a "non-free" hypothesis.
6. Validate and format: Run the provided bash scripts that invoke the Metamath program to validate and format your changes. These scripts are also used by GitHub Actions.
7. Push to your fork: Push your changes to your remote repository.
8. Check GitHub Actions: Verify if any errors are reported. If you encounter issues, feel free to share links to the errors here, and we’ll help you resolve them.
9. Iterate: Repeat the process until your branch passes all checks.
10. Submit a pull request (PR): Once everything looks good, create a PR to propose your changes for review.

With that, you’ll have your mathbox set up and ready for further contributions!

Again, welcome to the gang—we’re glad to have you here! 😊

Glauco

[Jim Kingdon]

On 1/12/25 07:46, Noam Pasman wrote:

Happy New Year!

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.

This probably will be a bit advanced based on what you say of your background, but I'd take at least a look at the HoTT Book at https://homotopytypetheory.org/book/ . Personally, I spent most time on chapters 1, 10, and 11 (section 11.6 is on surreal numbers). Sooner or later you'll run into type theory. I'm not sure it has to be sooner, though, so if the HoTT book seems incomprehensible, maybe go back to the books you mention above.

I wanted to ask about who I should contact in case I have a problem with setting everything up.

You found us! We have a few ways to communicate but this mailing list is probably best for that sort of question.

Eventually, I'd love to help with some project in the database if needed and if I already somewhat understand the concepts.. . . If there's another project that I'd be more useful for, that's good too!

To be honest I'm not completely sure what would make the best learning project. Maybe something like https://github.com/metamath/set.mm/issues/4384 or even https://github.com/metamath/set.mm/issues/4504 (which I mention mostly as a means to getting to know some of the metamath tools - renaming theorems isn't especially glamorous in terms of mathematical learning). You could also try re-proving some existing theorems or something else small. Feel free to browse https://github.com/metamath/set.mm/issues but if you start on something big and it seems overwhelming, look for a smaller project/task.

[Scott Fenton]

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

--
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 visit https://groups.google.com/d/msgid/metamath/CABJcXbRF5BsRyNC_hf3L_EmhmuSvfdaN3EKy%2BFOs10DLRUjPOg%40mail.gmail.com.

[Noam Pasman]

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

To view this discussion visit https://groups.google.com/d/msgid/metamath/CACKrHR-d%3DC7UHPvZZq0wYru0nzUF0PiZsZ-u8WbDrv0xCAmVFg%40mail.gmail.com.

[Andrew Thompson Thompson]

I always enjoyed Hamiton on logic, and Dedekind for set theory.  Really nice and easy introductions to the dark arts, and then you are ready for Russell and Whitehead's Principia.

Of course, for the hard-core you want to read "A Commentary on Thermodynamics" by Day.  A very thin Springer and Verlag Yellow book.  But it blows your mind when you see how he dispenses with the axioms and simply appeals to the language of smooth functions.  He later recovers the axioms and shows how simple analysis reveals the priors of Clausius and Duhem using nothing more than Lebesgue theory,.

Makes you wonder.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbQqhasoYyEi8tX_zZycDrhRgHU-OVF9LC-8_FSu%2BB7P-A%40mail.gmail.com.

[Noam Pasman]

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

[Jim Kingdon]

I run mmj2 using the https://github.com/digama0/mmj2/blob/master/mmj2jar/mmj2 script. It takes care of asking for enough memory, but from looking at the script it seems like the relevant option is

  -Xmx1280M

You'll probably also want a plain text editor capable of editing a file that big - two that have worked for me are vim and geany but I assume there are others.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CABJcXbSvK8FjiiHqg1RP8NL4tbLkqAhiVZtP291cd7xGSJZ2ww%40mail.gmail.com.

[Noam Pasman]

I switched to using that script and got it to work, but now I think I'm getting an error on the version of Java Runtime that I have? I'm not really sure what this means:

Exception in thread "main" java.lang.UnsupportedClassVersionError: mmj/util/BatchMMJ2 has been compiled by a more recent version of the Java Runtime (class file version 55.0), this version of the Java Runtime only recognizes class file versions up to 52.0
at java.lang.ClassLoader.defineClass1(Native Method)
at java.lang.ClassLoader.defineClass(ClassLoader.java:756)
at java.security.SecureClassLoader.defineClass(SecureClassLoader.java:142)
at java.net.URLClassLoader.defineClass(URLClassLoader.java:473)
at java.net.URLClassLoader.access$100(URLClassLoader.java:74)
at java.net.URLClassLoader$1.run(URLClassLoader.java:369)
at java.net.URLClassLoader$1.run(URLClassLoader.java:363)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:362)
at java.lang.ClassLoader.loadClass(ClassLoader.java:418)
at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:359)
at java.lang.ClassLoader.loadClass(ClassLoader.java:351)
at sun.launcher.LauncherHelper.checkAndLoadMain(LauncherHelper.java:641)

To view this discussion visit https://groups.google.com/d/msgid/metamath/5606860a-2156-4262-bad8-410559207ebe%40panix.com.

[savask]

I hope you'll be able to set up mmj2 (I've also been having some problems with making it run recently; it's essentially abandonware), but you could try an online proof assistant metamath-lamp in the meantime: https://github.com/expln/metamath-lamp It runs in your browser, and there are also several guides and videos on how to use it.

[Alexander van der Vekens]

Which Java version do you use? There were always problems with versions higher than 8 (search for "JDK" in this Google group). So maybe you should use JDK 8.

[Noam Pasman]

I think the Java version might have been the issue. I'll look into it more closely if I want to go back to mmj2, but for now I'll think I'll just use metamath-lamp. It's been much easier to get the hang of so far.

--
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 visit https://groups.google.com/d/msgid/metamath/cb47d3bb-bb33-4e81-8746-dd34e237ff54n%40googlegroups.com.

[Jim Kingdon]

I'm running mmj2 using Java 11 via the PopOS package openjdk-11-jdk (which is probably the same as the Ubuntu package of the same name).

But if LAMP is working for you, so much the easier.

[Noam Pasman]

I finally finished reading through the metamath-lamp guide and made a new mathbox in my forked repository, along with a first theorem! I then tried to run "scripts/rewrap set.mm" in Terminal but I got this error:

line 8: metamath: command not found

I assume this means I have to install metamath-exe? I downloaded it and tried to run "gcc *.c -o metamath" but got another error:

zsh: no matches found: *.c

Does this mean I don't have GCC and need to download it? Or is there a way to validate and format without it (preferably without metamath-exe entirely)?

[Jim Kingdon]

On 1/19/25 19:41, Noam Pasman wrote:

> line 8: metamath: command not found
> I assume this means I have to install metamath-exe?

Yup!

> I downloaded it and tried to run "gcc *.c -o metamath" but got another
> error:
> zsh: no matches found: *.c
> Does this mean I don't have GCC and need to download it?

The error means there are no files named *.c in the current directory.
Did you cd to the src directory? The version of the above command, at
least in the version of metamath-exe from git, is

cd src && gcc m*.c -o metamath

As for whether you have gcc, you can run "gcc -v" to print the gcc
version if gcc is available.

> Or is there a way to validate and format without it (preferably
> without metamath-exe entirely)?

You can make a github fork and push up a pull request to run the tests
there.

[Noam Pasman]

Ok, everything's worked except for actually using the scripts/rewrap command itself. Currently, I have one folder with two separate directories: one with my forked repository of set.mm, and one with my downloaded copy of metamath-exe (called set.mm and metamath respectively). I've been running the script from the set.mm directory, since that's where the script is located, but the script calls ./metamath at the beginning which seems to only work while in the metamath/src directory. The commands in the script then refer to a set.mm file, but there is no such file in the metamath/src directory (there is one that comes with the metamath directory and one in the set.mm directory that I've been editing and intend to eventually commit).

I think the error might be in where I put the directories? The script seems to have a precise notion of which directory is supposed to be where and I don't want to interfere with that too much.

[Thierry Arnoux]

You probably simply have to add metamath to your PATH environment variable.

--
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 visit https://groups.google.com/d/msgid/metamath/CABJcXbQDcHJDrZD3bXEQiC%3DuVtUfvAYRqQbPSXubDj5bej86Mw%40mail.gmail.com.

[Noam Pasman]

Ok, everything worked and I made a pull request! Hopefully nothing went wrong.