> *Lamp uses depth 4 by default, but I'm not sure whether it corresponds to metamath's depth 4.*
You can change this value on the Settings tab. For example, I usually use 100 as the default value for depth. The value to use depends on your browser settings and Metamath database you are working with. If you start getting out-of-memory errors or your browser becomes unresponsive, then you should decrease the default depth. But if this doesn’t happen, then you are fine to use bigger values of depth. Usually bigger values of depth don’t make much difference, but occasionally you can find a proof which would be impossible to find with smaller values of depth. So, I would recommend using bigger values of depth if this doesn’t cause any issues with your browser. > *It is able to fill in some basic steps occasionally, though often it doesn't behave as I expect it to behave.* Can you describe one or few such cases when lamp doesn't behave as you expect? I will try to find an explanation to lamp’s behavior, and check if it is not a bug. On Saturday, December 6, 2025 at 7:27:58 AM UTC+1 savask wrote: > > 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/eaf1f9e5-ae15-4c94-b28b-f9b6dbd456e6n%40googlegroups.com.
