Metamath Speedrun!

[Jia Ming]

I proved the first 100 theorems from set.mm in 38min 42 secs hehe (which is just all the implications, excluding the one labeled OLD) you can find the video here https://odysee.com/@jiaminglimjm:e/metamath-speedrun:6

Anyone else wanna try? I wanna go sub-30 minutes but I need to be incentivised by a little competition. The implications were SUPER fun to speedrun. Also, since metamath verifies so quickly, it's fair to those with slower computers unlike the other ITPs. I came up with these few rules:

1. No referring to notes during the speedrun

2. Use the original C executable

3. Memorizing prior to speedrun is allowed

4. Proofs can be done in any order, as long as they are the same ones

5. Timer stops when metamath verifies that all proofs are correct

but suggestions are welcome. I haven't tried mmj2 or the OpenAI one yet so I don't know if they would be as nice to speedrun on as the original verifier/assistant in C.

To be exact about which theorems are used, the .mm file is attached below.

[Jim Kingdon]

This is delightful.

I wonder if it would be feasible to pose other challenges. For example, constructing the real numbers - with all the set theory, rational numbers, etc, assumed but starting with http://us.metamath.org/mpeuni/df-np.html and with success being achieved when all of the axioms at http://us.metamath.org/mpeuni/mmcomplex.html are proved - need not be via the same intermediate theorems. Perhaps that is too hard.

As for mmj2, proof writing itself is plenty fast, but at least the way I use it there is some copy pasting and other fiddling that I do - which perhaps I could just relearn a different way for speedruns.

--
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 on the web visit https://groups.google.com/d/msgid/metamath/54dda360-fea5-481f-afc5-d78680ace05dn%40googlegroups.com.