I don't have any particular experience with Yamma or mmj2. I was mainly thinking back to my experiences with metamath-lamp, which runs in the browser and will obviously be more limited in just how far it can brute force. It has a set threshold past which it will give up on unifying a blank step, and instead spit out a warning with the last theorem it was attempting. When it does give up, it's usually stuff like syl32anc with lots of general hypotheses.
If you wanted a pathological test case that should mix up any unifier, I'd try writing a theorem with maybe a dozen hypotheses, some combinations of which share variables that don't appear in the final assertion, alongside a WIP proof with a lot of steps that can individually match any hypothesis, but with only one combination causing all the shared variables to line up correctly. The goal would be to rule out almost all possible shortcuts so it actually has to check most combinations. On Sat, Sep 27, 2025, 7:09 PM Glauco <[email protected]> wrote: > Hi Matthew, > > do you have a specific partial .mmp file where you would expect > unification to fail or take forever so that I can test it with Yamma? (so > far I've not been able to find one; with every new major update I try > unification in the proof of ~ fouriersw that's more than 1500 steps and > contains some steps with "many" hyps) > > I've loaded the proof of ~ segconeq that contains two steps justified by > ~ syl333anc . If I remove the labels and the refs from both steps, Yamma > finds them with no lag. Maybe I've not understood the example you were > referring to? > > Thanks in advance > Glauco > > p.s. > before trying what I call "step derivation" (not sure if mmj2 uses the > same nomenclature), all parsing nodes for all theorems in set.mm need to > be computed and in my slow VM it takes about one minute (it is done by a > separate > working thread in the background) > > -- > 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/61681cd8-f663-4bd3-b650-06d076be97b1n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/61681cd8-f663-4bd3-b650-06d076be97b1n%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 visit https://groups.google.com/d/msgid/metamath/CADBQv9bVn4%2BoFqt6ZaorWB9JnT%3D1gEyxjkyuKQwLtv%3DDCy4ECg%40mail.gmail.com.
