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 <https://expln.github.io/lamp/latest/index.html>. 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: > > 1. What proof assistant are you currently using? > > mmj2 > > > 1. 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). > > > 1. 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.
