Proof Assistants
Marlo Bruder
I wanted to ask you all 3 questions related to proof assistants:
- What proof assistant are you currently using?
- 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?
- What are some things you don't like about your proof assistant that future proof assistants should avoid?
The reason I ask these question is on one hand to create a useful thread for anyone else who might try to create a proof assistant in the future and on the other hand to gather some information for my own upcoming proof assistant called mmt1, with which I aim to create a modern remake of mmj2. This means that the core proof assistant functionality will remain (mostly) the same, while at the same time I want to add much more features that weren't possible when mmj2 was created.
As of right now the feature set includes:
- A build in theorem explorer: You can browse any database without having to generate html pages and open them in a separate program/window.
- A more modern editor: mmt1 uses monaco-editor, a standalone version of vscode's editor, enabling features such as multi-cursor editing and the ability to edit very large files.
- A more modern UI: Both in style and functionality. Including a tab system, so that you can have multiple editor and theorem explorer instances open at the same time.
- Preview unicode feature: While developing proofs you can activate a live unicode preview that will make reading your proofs easier.
- An extended .mmp syntax: You can now also express comments, headers, constant statements, variable statements, floating hypotheses, axioms and theorems with temporary variables/floating hypotheses.
- Add to database feature: You can add theorems, axioms, etc. to the database with the click of a single button. Together with the extended syntax this allows you to create entire metamath databases without ever touching a .mm file
- An easier installation: Installing mmt1 will be as simple as clicking an installer. No downloading old java versions or adjusting script parameters required.
Hopefully the first version of mmt1 will be ready in about 1 to 3 months. Until then I still want to add the following:
- Complete recreation of mmj2's unifier: As of right now mmt1 only has mmj2's original unifier (which is only able to fill in refs given an assertion and hypotheses)
- Preview unify: It would be useful to see a preview of what triggering the unifier will do within the unicode preview
- A more powerful search tool: Right now mmt1's search capabilities are still very limited
- mmj2's definition checker
- More overall polish: More settings, less hardcoded values, some nicer styling, etc.
As for the tech-stack I went with tauri 2.0 as my overarching framework, which means that most of the application is written in rust, while the ui is written using html/css/js (and displayed using the OS's webview). I also chose svelte 5 as my frontend framework to allow component based development and (as mentioned above) I went with monaco-editor as my editor.
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?
- 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?
- 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?
I hope that asking for these changes isn't too much given that I have not yet contributed to set.mm myself.
Best regards,
Marlo Bruder
Glauco
Hi Marlo,
I use Yamma (a VSCode extension).
A Unicode view would be great — I’ve been thinking about how to implement it, but I haven’t figured out an effective way to display it without taking up too much video space (which is already barely enough to show long wffs).
An even cooler idea might be to allow writing .mmp files directly in Unicode, with the PA translating them to ASCII under the hood.
This would also make it possible to define "custom" symbols specific to a given .mmp file — for example, you could locally define the Unicode integral symbol to represent one of the many integrals defined in set.mm.
Thierry Arnoux
Hi Marlo,
First of all, congratulations on starting/announcing your
project!
What proof assistant are you currently using?
I also use Yamma.
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?
Maybe it's obvious, but I like the fact that it's integrated in
the VsCode IDE.
What are some things you don't like about your proof assistant that future proof assistants should avoid?
In terms of features I'm missing, I would really like to have the "select smallest class/wff" feature I had in Emetamath. This should not be too hard, and I think this would be of great help.
The "one-click publish" feature you describe would be nice. With
Yamma we have to copy-paste the MMT files, a very acceptable
burden ! :)
Back in 2010 I wrote a plugin for Eclipse : http://emetamath.tirix.org/
It basically encapsulated MMJ2 and offered some of these nice features:
- browsing of the database by chapters and sections,
- syntax highlighting,
- several editor panes, native search/replace, etc.,
- navigation to theorem declaration using the contextual menu,
- hover-popup with information about the symbol/theorem,
- that "select class/wff" feature I mentioned above...
I later made a video showing those features: https://youtu.be/BsEyW3vBcsE
As for the tech-stack I went with tauri 2.0 as my overarching framework, which means that most of the application is written in rust, while the ui is written using html/css/js (and displayed using the OS's webview). I also chose svelte 5 as my frontend framework to allow component based development and (as mentioned above) I went with monaco-editor as my editor.
Are you using metamath-rs
as a library or rewriting it from scratch? Is the project going to
be open source?
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?
This is a signal to MMJ2 that it should use the more advanced
"auto-transformation" on those steps.
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?
My solution in "Emetamath" was to add a dialog for users to
choose the colors. I'm not sure how much in common you have with
vscode, but you might be able to set extension-specific settings,
using JSON files in the project's .vscode directory.
Good luck with your project!
_
Thierry
Jim Kingdon
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?
- 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?
- 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?
- 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?
Igor Ieskov
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=sharingAutomatically 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.
Marlo Bruder
In terms of features I'm missing, I would really like to have the "select smallest class/wff" feature I had in Emetamath. This should not be too hard, and I think this would be of great help.
Are you using metamath-rs as a library or rewriting it from scratch? Is the project going to be open source?
Steven Nguyen
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
assistants?
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
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.
> 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 metamath+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/metamath/2b0367b3-aaae-4a89-ab95-89da44be60edn%40googlegroups.com.
Marlo Bruder
Marlo Bruder