While we're talking about unifiers, I'm still in the market for one which is api based with a thin command line wrapper. For all the reasons people usually ask for api or cli:
1. The usual way I write code is with a text editor and a terminal, and I like that seperation 2. A command line lets a programmer see what an api can do before getting their hands dirty 3. A unifier api would allow a programmer to focus on the front end of a proof assistant (my personal conceit, since 2018, is that I'd like to see/write an Incredible Proof Machine <https://incredible.pm/> (vertex-edge-graph drag and drop toy proof assistant) with a Metamath back end, and, oh, maybe a maxGraph <https://www.npmjs.com/package/@maxgraph/core>front end). 4. The collection of dockerised Metamath command line tools <https://github.com/Antony74/metamath-docker> I (occasionally) maintain, is currently little more than a glorified collection of verifiers, with the sole exception of metamath.exe which can do pretty much everything except allow you to start a proof at the beginning or in the middle. Thanks for listening to this aside. I should stop procrastinating and get back to whatever it was I was doing with checkmm.cpp & .ts ;-) Best regards, Antony On Sun, Sep 28, 2025 at 1:54 AM Glauco <[email protected]> wrote: > If anyone has a particularly challenging step in a proof in set.mm where > the step derivation could fail, please let me know. I'd be happy to try it. > > As I've written, I usually check the largest proof I'm aware of and > perform step derivation for a step that has many hypotheses and it's in the > final part of the proof. Since it's at the end of the proof, the > backtracking has 1500+ candidates for every hypothesis. Furthermore, the > correct label is in the last part of set.mm, so tens of thousands of > labels have to be tried before a solution is found. > > But since I wrote the algorithm, I'm the worst person to try to test it, > so adversarial tests are welcome. > > -- > 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/e96ad325-e3c6-4689-9ad7-b5a25a2860a9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/e96ad325-e3c6-4689-9ad7-b5a25a2860a9n%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/CAJ48g%2BAuX91i6yBfzvrNgPPVVXHTUSod6vcTY%3DAZfocM_kZ%2BxQ%40mail.gmail.com.
