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 <https://us.metamath.org/mpeuni/4syl.html> 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 <https://us.metamath.org/mpeuni/syl333anc.html> with loads of hypotheses, since there are simply too many possibilities for matching.
In practice, there are a few mitigating factors: 1. A unifier can first check that the conclusion matches the final line of the candidate theorem. Most theorems are very particular, so heuristics like (e.g.) "the candidate theorem's conclusion must have no constant symbols not present in the proof step" can quickly filter out the vast majority of theorems, without having to scan for hypotheses at all. 2. Of the remaining theorems, most have few hypotheses, and it works to eat the cost of scanning through all prior steps. It can still become an issue if you have a very large proof, which is one of the reasons to break them up into lemmas past a certain point. 3. Of the theorems that do have lots of hypotheses, most have very particular hypotheses, such as "|- F/ x ph" or "|- A = ( blah ` x )" that cannot match very many prior steps. So the overall combinatorial explosion can be broken up into hypotheses that match smaller subsets of the prior steps. Matthew House On Sat, Sep 27, 2025 at 5:35 PM Marlo Bruder <[email protected]> wrote: > Hello everyone, > I'm currently in the process of creating a mmj2 style proof assistant and > I had another question. So far my unifier is able to: > > 1. Fill in step refs if the assertion and hypotheses are given > 2. Unify the assertion and hypotheses if the step ref is given > > Now I noticed that yammas unifier is able to do the following: > > When given the following mmp file: > > h1::test.2 |- ( ps -> ch ) > h2::test.1 |- ps > qed:: |- ch > > The unifier is able to do the following: > > h1::test.1 |- ( ps -> ch ) > h2::test.2 |- ps > qed:2,1:ax-mp |- ch > > As you can see, despite the fact that the qed step previously had no > hypotheses or step ref, the unifier was able to fill in both at the same > time. Now my question is: How is this possible in a short period of time? > Wouldn't the proof assistant have to look at every theorem in the database, > and then try a whole lot of possible combinations of previous lines and > hypotheses? That sounds like it would take forever. There are obviously > some optimizations to be done (like when one hypothesis does not match a > line, don't try it again), but even then my intuition tells me that it > would still take practically forever, since multiple hypotheses could match > multiple lines and each combination would have to be tried. Is there a > smarter, faster way (than what is essentially a smart brute force) of > achieving this that I am overlooking? > > Best regards, > Marlo Bruder > > -- > 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/ddc0991a-7f2d-4f50-92f4-e504e4f038c9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/ddc0991a-7f2d-4f50-92f4-e504e4f038c9n%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/CADBQv9bzPGu2wq6XQfH01S5M8Yfp6NGXmAr0%2Bdnowi8EtEZjsA%40mail.gmail.com.
