> Here is my video ... It was very interesting, thanks. For me the highlight of the video was the "proving bottom-up" dialog, which can search for proofs of large depth automatically. Metamath.exe also has one (the "improve" command), and mmj2 doesn't, as far as I'm aware, so in a sense metamath-lamp has partly surpassed mmj2 in functionality.
There was an interesting part near the end where the proof search couldn't figure out that A e. CC is implied by A e. RR, since the latter statement has the same length and hence isn't picked up by the "Less" search heuristic. I think mmj2's transformation script <https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js> can circumvent such issues in special cases, so there's potential for improving the search maybe by adding special tactics for set.mm which narrow down the search with specific theorems banned/allowed. > I proved the fifth theorem. Again, apparently one hypothesis is not needed, the set B is not required to be not empty. Nice! You shouldn't require nonemptyness until lemma 7, which postulates the existence of unity. I think it's a bit unfortunate that we allow empty magmas, since algebraic structures are usually assumed to be based on nonempty sets; this makes the theory more uniform. -- 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 visit https://groups.google.com/d/msgid/metamath/25756eb2-285c-4c49-8b07-ca9be49a3477n%40googlegroups.com.
