> I don't know about metamath lamp, but the search power of the metamath.exe 'improve' command is very minimal.
Lamp uses depth 4 by default, but I'm not sure whether it corresponds to metamath's depth 4. It is able to fill in some basic steps occasionally, though often it doesn't behave as I expect it to behave. > Depending on the decidability of GL (which I don't know), one could attempt writing tactics in Rumm as well. It is decidable, some sort of procedure is described in Boolos' chapter 10, though I haven't looked at it in detail. As for Rumm, I would love to contribute some tactics but my general feeling is that we no longer have a "widely accepted" and actively-developed proof assistant: mmj2 is abandoned, metamath-exe is also almost abandoned, metamath-knife seems to be stagnant as well with many pull requests lying around for years. This is probably a theme for another topic, but does anyone uses Rumm in their set.mm work? > Perhaps I can explain my way of thinking a bit, since sources for a proof of Day 20 seem to be scarce (spoilers start here): Thanks a lot! -- 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/db60ae06-a902-4293-badc-dd953c8f1131n%40googlegroups.com.
