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.
On 12/26/20 5:26 AM, Jia Ming wrote:
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.
--
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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/54dda360-fea5-481f-afc5-d78680ace05dn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/54dda360-fea5-481f-afc5-d78680ace05dn%40googlegroups.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 on the web visit
https://groups.google.com/d/msgid/metamath/1f9d7a20-a9bc-7f73-b538-56c569461310%40panix.com.
