1. What proof assistant are you currently using? I use metamath.exe (and notepad, for editing the comments, pasting proofs, etc.) I do have other proof assistants which have been useful in some uncommon situations
2. What are some (not so obvious) features of your proof assistant that you like and that you would like to see recreated in future proof assistants? I think metamath.exe is more efficient because of low dependence on mouse movement. It's basically a CLI, after all. For example, say you have 7 steps and you want to fill in `eqeq1` for all of them. This is as easy as running `a -0 eqeq1` to assign one step, then pressing "up arrow" then "enter" for the other steps. Similarly, if you want to fill in hypotheses `theorem.a` to `theorem.k`, just `a -0 theorem.a`, then do "up arrow" "backspace" "b" "enter", etc. Although setting an unknown expression to a value is often made faster by copying and pasting the expression instead of typing it out. So, I would suggest keyboard commands, for jumping around unknown steps, for searching, and for autoproving. And maybe some kind of view at the bottom showing only the unknown steps - in very long proofs, there might be a lot of scrolling along solved steps. I like metamath.exe's behaviour that when it tries to automatically prove something (`im all`) and fails, nothing happens. In contrast, mmj2 likes to do partial work, but it often does oveq123d, ending up with silly unprovable unknown steps.like `+ = x.` Alternatively, metamath-lamp explicitly lets you choose whatever subproof or partial work it found, or cancel(do not apply any step). 3. What are some things you don't like about your proof assistant that future proof assistants should avoid? metamath.exe is bad at proof editing: to change one step, you often need to reprove the whole subtree. But I don't think this will be a problem. A feature I would like is the ability to import partial proofs with "?" from metamath.exe to other tools. On Sun, Jun 8, 2025 at 7:34 AM Igor Ieskov <[email protected]> wrote: > > Hi Marlo, > > I am not really involved in creating metamath proofs. But whenever I want to > create one or to just explore existing proofs, I use metamath-lamp. I guess > the importance of features depends on experience. More experienced > metamathematicians will value some features more, less experienced will value > others. But I will list features of mm-lamp which I like and I think they > will be useful for all users. > > Proof editor: > > Syntax-aware selection. Probably, this is the same thing that Thierry > mentioned as “select smallest class/wff”. This feature allows one to quickly > explore the syntax of a statement “in-place” and quickly select some > meaningful part of a statement for copy/paste. This feature works as follows. > When you click a symbol in a statement, the smallest “meaningful” part of the > statement containing the clicked symbol gets selected. After that you can > expand selection (select the next smallest “meaningful” fragment containing > already selected fragment) or shrink selection (inverse of expanding). > > Fragment transformers. > https://lamp-guide.metamath.org/#transformers-more-than-meets-the-eye , > https://github.com/expln/metamath-lamp-docs/blob/master/mm_lamp_versions/v27/editor/transform_copy_for_deduction.md > > Possibility to automate some repetitive actions. You can write JavaScript > programs and embed them into the proof assistant to add custom functionality. > This is not documented, so this is currently one of the “not so obvious” > features. However, a few videos were made to show this capability: > https://drive.google.com/file/d/1c5t-Nhuy6KX6UmTtEGjXJa-54HFZhp3x/view?usp=drive_link > Starting at 7:58 > https://drive.google.com/file/d/17hEdfgvX-hcA13qdAgNps_29dew065kB/view?usp=sharing > > Automatically creating long proofs in some simple/obvious cases. This feature > is demonstrated in this video starting at 30:00 > https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing > (This video shows one issue at 32:45, when mm-lamp cannot prove that “B e. > RR” implies “B e. CC”. This issue is solved in the latest version of mm-lamp. > To make the same proof, instead of the usual bottom-up prover, you need to > use the “Prove” macro available in “default set.mm macros” in the latest > version of mm-lamp). > > Proof explorer: > > Visualizations of substitutions in each proof step. As for me, this greatly > simplifies understanding of proofs. In fact, as I don’t remember names and > meanings of assertions, visualizations are the only way I can follow proofs > in Metamath. > > Search by pattern https://lamp-guide.metamath.org/#search-patterns , > https://github.com/expln/metamath-lamp-docs/blob/master/mm_lamp_versions/v27/explorer/search_by_pattern.md > > Combination of the “syntax-aware selection” and the “search by pattern”. You > can quickly select a fragment of a statement using syntax-aware selection and > click the Search button. This will open a new explorer tab showing all > assertions with statements containing “similar” fragments. Often the search > result includes the syntax definition for the selected fragment (if it was > short enough) and examples of usage which helps understanding how to use that > syntax. > https://github.com/expln/metamath-lamp-docs/blob/master/mm_lamp_versions/v27/explorer/multiple_explorer_tabs.md > > You can also find out more useful features by reading Metamath-lamp Guide > https://lamp-guide.metamath.org Some recently added features not mentioned in > the guide, can be found in metamath-lamp-docs > https://github.com/expln/metamath-lamp-docs . > > If you need to know how to do one or another thing/action in mm-lamp or how > something is implemented, feel free to ask me, I'll be happy to help you. > > - > Igor > > On Sunday, June 8, 2025 at 7:09:36 AM UTC+2 [email protected] wrote: >> >> On 6/6/25 22:42, Marlo Bruder wrote: >> >> Hello there metamath community! >> >> I wanted to ask you all 3 questions related to proof assistants: >> >> What proof assistant are you currently using? >> >> mmj2 >> >> What are some (not so obvious) features of your proof assistant that you >> like and that you would like to see recreated in future proof assistants? >> >> The screen is mostly devoted to my proof, with a minimal space taken up by >> navigation widgets and the like. >> >> I can copy-paste .mmp files between set.mm and iset.mm and, insofar as the >> theorems being referenced are present in both, it works. >> >> This one is kinda dumb but I'll state it anyway: the format of the generated >> proof differs visually (in line length) from the output of a minimized proof >> from the metamath-exe minimizer, which I use to notice whether I forgot to >> run the minimizer. >> >> I use comments (lines starting with "*") extensively (to make notes to >> myself, comment out proof lines, etc). >> >> What are some things you don't like about your proof assistant that future >> proof assistants should avoid? >> >> Ideally the proof assistant would be a bit better able to fill in certain >> things like substitutions (in fact, under some circumstances I think older >> versions of mmj2 were better than the one I am using now). >> >> mmj2 has a lot of rough edges (menu items that don't work, keystrokes which >> can destroy your proof unless it was saved, etc). Perhaps it goes without >> saying that I'd prefer not to have such things but maybe the larger lesson >> is to focus on fixing annoyances as much as implementing more features. >> >> >> >> Lastly I still had a few more questions about metamath and set.mm: >> >> What does the ! at the beginning of statements do in mmj2? I think I read >> somewhere that it was an undocumented change. Is anyone nevertheless able to >> come up with an informal description of how it impacts the unifier? >> >> It tells mmj2 to try to find a proof for this step. Without the "!" mmj2 >> will mostly leave the line alone, without proving it in terms of previous >> steps. I use this for example when there are steps in the proof which I know >> I can't prove, but which I'm not ready to comment out yet (and thus I don't >> want the line without ! to pick them up). >> >> I want to be able to syntax highlight variables without having to hardcode >> the colors. Right now it seems the only way I can do this would be to parse >> the htmlvarcolor setting, which would be pretty tedious. Would it be >> possible to add a varcolorcode setting to the typesetting comment, which >> assigns a variable colorcode to a typecode? And if not: How does mmj2 derive >> the colors for it's syntax highlighting? Are they hardcoded? >> >> Don't know about mmj2 but strikes me as sensible to add something like >> varcolorcode. >> >> In mmt1 the table of contents is replaced by an explorer on the left side of >> the screen, similar to e.g. vscode's file explorer, only with headers >> instead of folders. This however requires that all headers are exactly one >> header depth below their parent header. set.mm follows this rule in with all >> headers but 3 in Jim Kingdom's mathbox. Would it be ok (specifically for Jim >> Kingdom himself) to change the header depth of those 3 headers? >> >> Ideally we'd have a tool to enforce this which we can run on pull requests, >> but seems like a good idea. If I get around it I'll fix it but if you want >> to make a pull request to my mathbox that's fine too. >> > -- > 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/2b0367b3-aaae-4a89-ab95-89da44be60edn%40googlegroups.com. -- 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/CAAfCLnjCwkPTTO5itPXW8Mg7udM_WOfu%2BRM1HNY4qY5EaoipYg%40mail.gmail.com.
