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].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/54dda360-fea5-481f-afc5-d78680ace05dn%40googlegroups.com.
$c ( $.
$c ) $.
$c -> $.
$c -. $.
$c wff $.
$c |- $.
$v ph $.
$v ps $.
$v ch $.
$v th $.
$v ta $.
$v et $.
$v ze $.
$v si $.
$v rh $.
$v mu $.
$v la $.
$v ka $.
wph $f wff ph $.
wps $f wff ps $.
wch $f wff ch $.
wth $f wff th $.
wta $f wff ta $.
wet $f wff et $.
wze $f wff ze $.
wsi $f wff si $.
wrh $f wff rh $.
wmu $f wff mu $.
wla $f wff la $.
wka $f wff ka $.
${
dummylink.1 $e |- ph $.
dummylink.2 $e |- ps $.
dummylink $p |- ph $= $.
$}
${
idi.1 $e |- ph $.
idi $p |- ph $= $.
$}
wn $a wff -. ph $.
wi $a wff ( ph -> ps ) $.
${
min $e |- ph $.
maj $e |- ( ph -> ps ) $.
ax-mp $a |- ps $.
$}
ax-1 $a |- ( ph -> ( ps -> ph ) ) $.
ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $.
$( ax-3 $a |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) $. $)
${
mp2.1 $e |- ph $.
mp2.2 $e |- ps $.
mp2.3 $e |- ( ph -> ( ps -> ch ) ) $.
mp2 $p |- ch $= $.
$}
${
mp2b.1 $e |- ph $.
mp2b.2 $e |- ( ph -> ps ) $.
mp2b.3 $e |- ( ps -> ch ) $.
mp2b $p |- ch $= $.
$}
${
a1i.1 $e |- ph $.
a1i $p |- ( ps -> ph ) $= $.
$}
${
2a1i.1 $e |- ph $.
2a1i $p |- ( ps -> ( ch -> ph ) ) $= $.
$}
${
mp1i.1 $e |- ph $.
mp1i.2 $e |- ( ph -> ps ) $.
mp1i $p |- ( ch -> ps ) $= $.
$}
${
a2i.1 $e |- ( ph -> ( ps -> ch ) ) $.
a2i $p |- ( ( ph -> ps ) -> ( ph -> ch ) ) $= $.
$}
${
mpd.1 $e |- ( ph -> ps ) $.
mpd.2 $e |- ( ph -> ( ps -> ch ) ) $.
mpd $p |- ( ph -> ch ) $= $.
$}
${
imim2i.1 $e |- ( ph -> ps ) $.
imim2i $p |- ( ( ch -> ph ) -> ( ch -> ps ) ) $= $.
$}
${
syl.1 $e |- ( ph -> ps ) $.
syl.2 $e |- ( ps -> ch ) $.
syl $p |- ( ph -> ch ) $= $.
$}
${
3syl.1 $e |- ( ph -> ps ) $.
3syl.2 $e |- ( ps -> ch ) $.
3syl.3 $e |- ( ch -> th ) $.
3syl $p |- ( ph -> th ) $= $.
$}
${
4syl.1 $e |- ( ph -> ps ) $.
4syl.2 $e |- ( ps -> ch ) $.
4syl.3 $e |- ( ch -> th ) $.
4syl.4 $e |- ( th -> ta ) $.
4syl $p |- ( ph -> ta ) $= $.
$}
$( 2a1OLD $p |- ( ph -> ( ps -> ( ch -> ph ) ) ) $= $. $)
${
mpi.1 $e |- ps $.
mpi.2 $e |- ( ph -> ( ps -> ch ) ) $.
mpi $p |- ( ph -> ch ) $= $.
$}
${
mpisyl.1 $e |- ( ph -> ps ) $.
mpisyl.2 $e |- ch $.
mpisyl.3 $e |- ( ps -> ( ch -> th ) ) $.
mpisyl $p |- ( ph -> th ) $= $.
$}
id $p |- ( ph -> ph ) $= $.
id1 $p |- ( ph -> ph ) $= $.
idd $p |- ( ph -> ( ps -> ps ) ) $= $.
${
a1d.1 $e |- ( ph -> ps ) $.
a1d $p |- ( ph -> ( ch -> ps ) ) $= $.
$}
${
2a1d.1 $e |- ( ph -> ps ) $.
2a1d $p |- ( ph -> ( ch -> ( th -> ps ) ) ) $= $.
$}
2a1 $p |- ( ph -> ( ps -> ( ch -> ph ) ) ) $= $.
${
a2d.1 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
a2d $p |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) ) $= $.
$}
${
sylcom.1 $e |- ( ph -> ( ps -> ch ) ) $.
sylcom.2 $e |- ( ps -> ( ch -> th ) ) $.
sylcom $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
syl5com.1 $e |- ( ph -> ps ) $.
syl5com.2 $e |- ( ch -> ( ps -> th ) ) $.
syl5com $p |- ( ph -> ( ch -> th ) ) $= $.
$}
${
com12.1 $e |- ( ph -> ( ps -> ch ) ) $.
com12 $p |- ( ps -> ( ph -> ch ) ) $= $.
$}
${
syl5.1 $e |- ( ph -> ps ) $.
syl5.2 $e |- ( ch -> ( ps -> th ) ) $.
syl5 $p |- ( ch -> ( ph -> th ) ) $= $.
$}
${
syl6.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl6.2 $e |- ( ch -> th ) $.
syl6 $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
syl56.1 $e |- ( ph -> ps ) $.
syl56.2 $e |- ( ch -> ( ps -> th ) ) $.
syl56.3 $e |- ( th -> ta ) $.
syl56 $p |- ( ch -> ( ph -> ta ) ) $= $.
$}
${
syl6com.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl6com.2 $e |- ( ch -> th ) $.
syl6com $p |- ( ps -> ( ph -> th ) ) $= $.
$}
${
mpcom.1 $e |- ( ps -> ph ) $.
mpcom.2 $e |- ( ph -> ( ps -> ch ) ) $.
mpcom $p |- ( ps -> ch ) $= $.
$}
${
syli.1 $e |- ( ps -> ( ph -> ch ) ) $.
syli.2 $e |- ( ch -> ( ph -> th ) ) $.
syli $p |- ( ps -> ( ph -> th ) ) $= $.
$}
${
syl2im.1 $e |- ( ph -> ps ) $.
syl2im.2 $e |- ( ch -> th ) $.
syl2im.3 $e |- ( ps -> ( th -> ta ) ) $.
syl2im $p |- ( ph -> ( ch -> ta ) ) $= $.
$}
pm2.27 $p |- ( ph -> ( ( ph -> ps ) -> ps ) ) $= $.
${
mpdd.1 $e |- ( ph -> ( ps -> ch ) ) $.
mpdd.2 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
mpdd $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
mpid.1 $e |- ( ph -> ch ) $.
mpid.2 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
mpid $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
mpdi.1 $e |- ( ps -> ch ) $.
mpdi.2 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
mpdi $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
mpii.1 $e |- ch $.
mpii.2 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
mpii $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
syld.1 $e |- ( ph -> ( ps -> ch ) ) $.
syld.2 $e |- ( ph -> ( ch -> th ) ) $.
syld $p |- ( ph -> ( ps -> th ) ) $= $.
$}
${
mp2d.1 $e |- ( ph -> ps ) $.
mp2d.2 $e |- ( ph -> ch ) $.
mp2d.3 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
mp2d $p |- ( ph -> th ) $= $.
$}
${
a1dd.1 $e |- ( ph -> ( ps -> ch ) ) $.
a1dd $p |- ( ph -> ( ps -> ( th -> ch ) ) ) $= $.
$}
${
2a1dd.1 $e |- ( ph -> ( ps -> ch ) ) $.
2a1dd $p |- ( ph -> ( ps -> ( th -> ( ta -> ch ) ) ) ) $= $.
$}
${
pm2.43i.1 $e |- ( ph -> ( ph -> ps ) ) $.
pm2.43i $p |- ( ph -> ps ) $= $.
$}
${
pm2.43d.1 $e |- ( ph -> ( ps -> ( ps -> ch ) ) ) $.
pm2.43d $p |- ( ph -> ( ps -> ch ) ) $= $.
$}
${
pm2.43a.1 $e |- ( ps -> ( ph -> ( ps -> ch ) ) ) $.
pm2.43a $p |- ( ps -> ( ph -> ch ) ) $= $.
$}
${
pm2.43b.1 $e |- ( ps -> ( ph -> ( ps -> ch ) ) ) $.
pm2.43b $p |- ( ph -> ( ps -> ch ) ) $= $.
$}
pm2.43 $p |- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) ) $= $.
${
imim2d.1 $e |- ( ph -> ( ps -> ch ) ) $.
imim2d $p |- ( ph -> ( ( th -> ps ) -> ( th -> ch ) ) ) $= $.
$}
imim2 $p |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) ) $= $.
${
embantd.1 $e |- ( ph -> ps ) $.
embantd.2 $e |- ( ph -> ( ch -> th ) ) $.
embantd $p |- ( ph -> ( ( ps -> ch ) -> th ) ) $= $.
$}
${
3syld.1 $e |- ( ph -> ( ps -> ch ) ) $.
3syld.2 $e |- ( ph -> ( ch -> th ) ) $.
3syld.3 $e |- ( ph -> ( th -> ta ) ) $.
3syld $p |- ( ph -> ( ps -> ta ) ) $= $.
$}
${
sylsyld.1 $e |- ( ph -> ps ) $.
sylsyld.2 $e |- ( ph -> ( ch -> th ) ) $.
sylsyld.3 $e |- ( ps -> ( th -> ta ) ) $.
sylsyld $p |- ( ph -> ( ch -> ta ) ) $= $.
$}
${
imim12i.1 $e |- ( ph -> ps ) $.
imim12i.2 $e |- ( ch -> th ) $.
imim12i $p |- ( ( ps -> ch ) -> ( ph -> th ) ) $= $.
$}
${
imim1i.1 $e |- ( ph -> ps ) $.
imim1i $p |- ( ( ps -> ch ) -> ( ph -> ch ) ) $= $.
$}
${
imim3i.1 $e |- ( ph -> ( ps -> ch ) ) $.
imim3i $p |- ( ( th -> ph ) -> ( ( th -> ps ) -> ( th -> ch ) ) ) $= $.
$}
${
sylc.1 $e |- ( ph -> ps ) $.
sylc.2 $e |- ( ph -> ch ) $.
sylc.3 $e |- ( ps -> ( ch -> th ) ) $.
sylc $p |- ( ph -> th ) $= $.
$}
${
syl3c.1 $e |- ( ph -> ps ) $.
syl3c.2 $e |- ( ph -> ch ) $.
syl3c.3 $e |- ( ph -> th ) $.
syl3c.4 $e |- ( ps -> ( ch -> ( th -> ta ) ) ) $.
syl3c $p |- ( ph -> ta ) $= $.
$}
${
syl6mpi.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl6mpi.2 $e |- th $.
syl6mpi.3 $e |- ( ch -> ( th -> ta ) ) $.
syl6mpi $p |- ( ph -> ( ps -> ta ) ) $= $.
$}
${
mpsyl.1 $e |- ph $.
mpsyl.2 $e |- ( ps -> ch ) $.
mpsyl.3 $e |- ( ph -> ( ch -> th ) ) $.
mpsyl $p |- ( ps -> th ) $= $.
$}
${
syl6c.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl6c.2 $e |- ( ph -> ( ps -> th ) ) $.
syl6c.3 $e |- ( ch -> ( th -> ta ) ) $.
syl6c $p |- ( ph -> ( ps -> ta ) ) $= $.
$}
${
syl6ci.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl6ci.2 $e |- ( ph -> th ) $.
syl6ci.3 $e |- ( ch -> ( th -> ta ) ) $.
syl6ci $p |- ( ph -> ( ps -> ta ) ) $= $.
$}
${
syldd.1 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
syldd.2 $e |- ( ph -> ( ps -> ( th -> ta ) ) ) $.
syldd $p |- ( ph -> ( ps -> ( ch -> ta ) ) ) $= $.
$}
${
syl5d.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl5d.2 $e |- ( ph -> ( th -> ( ch -> ta ) ) ) $.
syl5d $p |- ( ph -> ( th -> ( ps -> ta ) ) ) $= $.
$}
${
syl7.1 $e |- ( ph -> ps ) $.
syl7.2 $e |- ( ch -> ( th -> ( ps -> ta ) ) ) $.
syl7 $p |- ( ch -> ( th -> ( ph -> ta ) ) ) $= $.
$}
${
syl6d.1 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
syl6d.2 $e |- ( ph -> ( th -> ta ) ) $.
syl6d $p |- ( ph -> ( ps -> ( ch -> ta ) ) ) $= $.
$}
${
syl8.1 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
syl8.2 $e |- ( th -> ta ) $.
syl8 $p |- ( ph -> ( ps -> ( ch -> ta ) ) ) $= $.
$}
${
syl9.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl9.2 $e |- ( th -> ( ch -> ta ) ) $.
syl9 $p |- ( ph -> ( th -> ( ps -> ta ) ) ) $= $.
$}
${
syl9r.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl9r.2 $e |- ( th -> ( ch -> ta ) ) $.
syl9r $p |- ( th -> ( ph -> ( ps -> ta ) ) ) $= $.
$}
${
syl10.1 $e |- ( ph -> ( ps -> ch ) ) $.
syl10.2 $e |- ( ph -> ( ps -> ( th -> ta ) ) ) $.
syl10.3 $e |- ( ch -> ( ta -> et ) ) $.
syl10 $p |- ( ph -> ( ps -> ( th -> et ) ) ) $= $.
$}
${
a1ddd.1 $e |- ( ph -> ( ps -> ( ch -> ta ) ) ) $.
a1ddd $p |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) ) $= $.
$}
${
imim12d.1 $e |- ( ph -> ( ps -> ch ) ) $.
imim12d.2 $e |- ( ph -> ( th -> ta ) ) $.
imim12d $p |- ( ph -> ( ( ch -> th ) -> ( ps -> ta ) ) ) $= $.
$}
${
imim1d.1 $e |- ( ph -> ( ps -> ch ) ) $.
imim1d $p |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) ) $= $.
$}
imim1 $p |- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) $= $.
pm2.83 $p |- ( ( ph -> ( ps -> ch ) )
-> ( ( ph -> ( ch -> th ) ) -> ( ph -> ( ps -> th ) ) ) ) $= $.
${
com3.1 $e |- ( ph -> ( ps -> ( ch -> th ) ) ) $.
com23 $p |- ( ph -> ( ch -> ( ps -> th ) ) ) $= $.
com3r $p |- ( ch -> ( ph -> ( ps -> th ) ) ) $= $.
com13 $p |- ( ch -> ( ps -> ( ph -> th ) ) ) $= $.
com3l $p |- ( ps -> ( ch -> ( ph -> th ) ) ) $= $.
$}
pm2.04 $p |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) ) $= $.
${
com4.1 $e |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) ) $.
com34 $p |- ( ph -> ( ps -> ( th -> ( ch -> ta ) ) ) ) $= $.
com4l $p |- ( ps -> ( ch -> ( th -> ( ph -> ta ) ) ) ) $= $.
com4t $p |- ( ch -> ( th -> ( ph -> ( ps -> ta ) ) ) ) $= $.
com4r $p |- ( th -> ( ph -> ( ps -> ( ch -> ta ) ) ) ) $= $.
com24 $p |- ( ph -> ( th -> ( ch -> ( ps -> ta ) ) ) ) $= $.
com14 $p |- ( th -> ( ps -> ( ch -> ( ph -> ta ) ) ) ) $= $.
$}
${
com5.1 $e |- ( ph -> ( ps -> ( ch -> ( th -> ( ta -> et ) ) ) ) ) $.
com45 $p |- ( ph -> ( ps -> ( ch -> ( ta -> ( th -> et ) ) ) ) ) $= $.
com35 $p |- ( ph -> ( ps -> ( ta -> ( th -> ( ch -> et ) ) ) ) ) $= $.
com25 $p |- ( ph -> ( ta -> ( ch -> ( th -> ( ps -> et ) ) ) ) ) $= $.
com5l $p |- ( ps -> ( ch -> ( th -> ( ta -> ( ph -> et ) ) ) ) ) $= $.
com15 $p |- ( ta -> ( ps -> ( ch -> ( th -> ( ph -> et ) ) ) ) ) $= $.
com52l $p |- ( ch -> ( th -> ( ta -> ( ph -> ( ps -> et ) ) ) ) ) $= $.
com52r $p |- ( th -> ( ta -> ( ph -> ( ps -> ( ch -> et ) ) ) ) ) $= $.
com5r $p |- ( ta -> ( ph -> ( ps -> ( ch -> ( th -> et ) ) ) ) ) $= $.
$}
imim12 $p |- ( ( ph -> ps ) ->
( ( ch -> th ) -> ( ( ps -> ch ) -> ( ph -> th ) ) ) ) $= $.
jarr $p |- ( ( ( ph -> ps ) -> ch ) -> ( ps -> ch ) ) $= $.
${
pm2.86d.1 $e |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) ) $.
pm2.86d $p |- ( ph -> ( ps -> ( ch -> th ) ) ) $= $.
$}
pm2.86 $p |- ( ( ( ph -> ps ) -> ( ph -> ch ) ) ->
( ph -> ( ps -> ch ) ) ) $= $.
${
pm2.86i.1 $e |- ( ( ph -> ps ) -> ( ph -> ch ) ) $.
pm2.86i $p |- ( ph -> ( ps -> ch ) ) $= $.
pm2.86iALT $p |- ( ph -> ( ps -> ch ) ) $= $.
$}
loolin $p |- ( ( ( ph -> ps ) -> ( ps -> ph ) ) -> ( ps -> ph ) ) $= $.
loowoz $p |- ( ( ( ph -> ps ) -> ( ph -> ch ) )
-> ( ( ps -> ph ) -> ( ps -> ch ) ) ) $= $.
