Thanks for confirming that it is just a smart brute force, erveryone! The algorithm is not implemented.
Best regards, Marlo Bruder On Tuesday, September 30, 2025 at 10:26:38 PM UTC+2 [email protected] wrote: > > My understanding is that it really is just a smart brute force: the > worst-case time complexity is something like O((# of theorems) × (# of > preceding steps) ^ (# of hypotheses per theorem)). That's why 4syl is > discouraged, since both its hypotheses and conclusion are very broad and > can potentially match many different steps. In my experience with > metamath-lamp's unifier, it tends to time out on theorems like syl333anc > with loads of hypotheses, since there are simply too many possibilities for > matching. > > Yes, that’s correct, in metamath-lamp it is just a smart brute force. I > need to check, but I feel like the inability to unify syl333anc and similar > assertions in some cases is not the browser limitation, it is rather not > enough optimized implementation. > > Maybe this will be useful: > > 1. In this comment > <https://github.com/expln/metamath-lamp/issues/77#issuecomment-1577804381> > Mario summarized his implementation of the unification algorithm in MM1. > 2. This comment > <https://github.com/expln/metamath-lamp/issues/77#issuecomment-1608487072> > contains a few interesting examples of unification. > > > - > Igor > > -- 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/57a24cae-2786-422b-a44c-03e58f4c285an%40googlegroups.com.
