On Sun, Sep 28, 2025 at 11:29 AM Marlo Bruder <[email protected]> wrote:
> Hey Antony, > > While we're talking about unifiers, I'm still in the market for one which > is api based with a thin command line wrapper. > > > Could you elaborate on your proposal a bit? When you say "thin command > line wrapper", do you mean a fully functional proof assistant (like a > minimalist metamath.exe) or simply a command line tool that let's you call > the proof assistant functionality (unify step, renumber, etc.)? > At its most fundamental level, a unifier takes a .mm file and an incomplete .uue file and returns a hopefully slightly more complete .uue file, doesn't it? That's what I'd like to see from a command line tool. And if it could do more, that would be a bonus. Combined with your preferred text editor, this does indeed become the bare bones of a proof assistant. And I suggested it would also be nice to have a unifier as an api, in which case the cli just becomes a thin wrapper over that api. This is functionality which exists in at least three places - mmj2 (Mel O'Cat, Java) , yamma (Glauco, JavaScript), and metamath-vspa (Thierry, Rust). But to the best of my knowledge it has not been componentised and exposed in the kind of manner I was asking for, but it'd be nice to be wrong about that. > > > 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). > > > Another interesting proposal. Are you suggesting a drag and drop proof > assistant where the proof lines are represented as vertices and hypothesis > dependencies as edges? What would the advantage of such a proof assistant > be in your opinion? > I just found The Incredible Proof Machine to be a fun introduction to formal verifiers, and think it would be great with Metamath behind it. It might not have any utility beyond engaging beginners, given that the Scratch programming language gives a visual introduction to programming which people quickly move beyond to something which is text file based, but the proof diagrams would still be pretty. -- 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%2BBqUWy7HFgmYfAg5F_ObHTcM0xekAwrMbwwK--zXyAu-g%40mail.gmail.com.
