There is a follow up video https://youtu.be/OAXjsUZoOgo (7 hours!), where he attempts to prove 2+2 = 4 using the axiomatization of peano.mm. This was an unfortunate choice, because peano.mm has a bizarre axiomatization, uses polish notation for no apparent reason, and has *no theorems*, meaning that even the most basic propositional logic is not available without a huge effort. If the addition axioms had been stated with term variables the proof of 2+2=4 would have been relatively straightforward, but instead he spends several hours trying to come to grips with peano.mm's idiosyncratic predicate logic formalization. And of course like any programmer he periodically google searches for things and of course comes up empty. Even searching for "metamath ide" multiple times yielded pretty inconclusive results, with some asteroid meta stuff pointing to a geocities dead link about mmide... Somehow we have to clean up our story here.
I don't have a MacOS machine so I would appreciate the attention of someone who knows their way around one to set up the scripts. The readme on github is actually borrowed directly from Mel's original readme, and is woefully out of date. Any scripts that I don't use are likely to have bit-rotted. He had to remove the -Xincgc option from the java call, and then it ran out of memory on set.mm. Possibly the memory limits in the script are out of date? This is a really good view at the newbie experience, from someone with a LOT of perseverence. The biggest question on his mind most of the time seems to be "how do people write this?" He's absolutely right that the syntax of metamath is almost adversarial, and he spends a lot of time constructing expressions in the pt 4 video by hand. I think we need to find a way to present this so that we don't ever give the impression that proof blocks are written by humans. He spends his time on miu.mm, then peano.mm, because these are the smallest databases, but I think this is unfortunate because they are both rather unusual by metamath standards. set.mm would have been an optimal starting point, except it's HUGE, which makes introductory stuff harder. Even worse, it starts with a comment that is tens of thousands of lines long, which makes it very difficult to see how "baby's first propositional logic" is supposed to go. I think we should try to curate a small selection of set.mm propositional logic and predicate logic, enough so that you have all the main theorems but not going for absolute saturation, with interstitial "tutorial" comments explaining the anatomy of an mm file along the way. Mario On Sun, Dec 22, 2019 at 8:26 AM savask <[email protected]> wrote: > I watched though the video and spotted a few things not mentioned in > Wolf's notes. > > At around 1:02 (1 hour 2 minutes), he starts writing a grammar file based > on the EBNF in the Metamath book. The book uses dashes inside symbols on > the left hand side of each rule, which is apparently not shared by all EBNF > standards, so he has to replace them by underscores. GNU bison supports > dashes (but calls it a GNU extension, incompatible with POSIX Yacc), Happy > parser verifier (for Haskell) also doesn't allow dashes in symbol names. > Maybe it is worthwhile replacing dashes by underscores in the Metamath book > EBNF? It may save someone time, in case if they would like to simply copy > the grammar file from the book. > > At 5:02, he tries mmj2. Apparently there's some sort of trouble launching > it on the MacOS (he had to modify the starting script), so maybe that bug > should be fixed. > > My impression is that most of his complaints come from missing > proof-assisting capabilities of the metamath program and mmj2, but main > points stand of course. Our tooling is scarce and most of work is done > manually anyway. On the other hand, the video has quite a lot of praise for > the Metamath book and the design of the language itself (stressing its > simplicity), so Metamath clearly has its strong points in comparison with > other proof systems. > > -- > 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/b2f84723-5ae7-4889-9403-176463bb5fb6%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b2f84723-5ae7-4889-9403-176463bb5fb6%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/CAFXXJStvN-fUJHuE_Ngz5B-WPCww-JVyyLM1jOHi40znZMNe3A%40mail.gmail.com.
