Hello metamath community, today I'm happy to announce the release of a new mmj2 style proof assistant called mmt1. The goal of mmt1 is to provide a more modern proof assistant experience than mmj2, by replicating what made mmj2 great, while adding new features to make it even better. These new features include a build in theorem explorer, an Unicode preview and the ability to add theorems to the database with only a few clicks.
For the Github repository and install instructions see: https://github.com/marloBruder/mmt1 The full feature set includes: - A build in theorem explorer: Including all the features you know from the web pages: Such as axiom/definition dependencies, references, indention, theorem numbers, etc. - A mmj2 style proof assistant: mmj2s unifier returns. The two big differences being an updated header syntax (similar to that of yamma) and an updated work variable syntax, to eliminate the potential for name conflicts. - An Unicode preview: To assist you during proof development, you can optionally active an Unicode preview. Apart from being able to read your proof in Unicode representation, you can also see axiom/definition dependencies, what parts of your proofs are finished/still have errors and a preview of what the unifier will do. Additionally, the Unicode preview can be popped out into a separate window, allowing you to place it on a second monitor (for the most optimal mmt1 experience). - A more modern editor: mmt1 uses monaco editor, which is a standalone version of vscodes editor. This means that you have access to vscodes very useful shortcuts, multi-cursor editing and can also edit large .mm files right within mmt1. - Search by parse tree: mmt1's main search feature allows you to search the database by whether statements contain or match certain parse tree snippets. - Add to database: You can add statements to the database automatically. Additionally, the proof assistant will show you a diff view of what is being changed, so that you can be sure that mmt1 is making the right edits. - An extended mmp syntax: mmt1 allows you to not just express theorems using .mmp files, but also axioms, floating hypotheses, variables, constants, comments and header. Combined with the add to database feature, this allows you to create entire metamath databases without ever touching an .mm file. Features still missing: - Definition checker: There appears to be an ongoing discussion about what definitions should look like in metamath, which is why I have held off on implementing the definition checker until the discussion is resolved. - Complete recreation of mmj2s unifier: The '!' feature is mainly still incomplete. Right now it only enables hypothesis finding (as in when the step ref is missing, the unifier will try out theorems which hypothesis amount differs from the one provided in the proof line). As far as I'm aware the '!' feature in mmj2 also enables a more advanced prover, which is currently not implemented in mmt1. - Automation: mmt1 currently does not support any kind of advanced automation such as a scripting language. - Inspect step: I eventually want to implement a feature for the theorem explorer that let's you inspect a proof step and shows you the exact substitutions made, what the theorem that was used looks like, etc. This should make it easier to follow complex proofs and should also help beginners understand metamath. - More search options: mmt1s current search capabilities should be good enough for a start, but they could be a lot greater. Moreover, in the future it would be great if mmt1s search could not just be used for aiding in proof development, but also for full on database exploration. - Add to database limitation: Right now the add to database feature only works when the statement can be inserted into the outer most scope, so if you for example try to insert a theorem between two theorems sharing a scope you will get an error and you will have to add your theorem manually. - Advanced database management: Right now you can only add statements to the database, but in the future it would be great if you could also edit, delete and move statements. This would then allow you to not just create, but also easily manage entire metamath databases right from within mmt1. - Select smallest wff/class: This was a feature requested in my original 'Proof Assistants' thread, but due to time constraints I haven't been able to implement it yet. - Many more shortcuts for .mmp files: Another feature requested in the original thread that I want to eventually implement. - Move file/folder: Right now you can't move files or folders around in the file explorer. This is mainly missing due to the complexity of the required drag and drop mechanism. - Command line tool: At the moment the only way to interact with mmt1s logic is through the UI. In the future it might make sense to create a command line tool to interact with it as well. Current limitations: - Long database opening time: Opening set.mm takes about a full minute on my laptop, which is relatively fast. On older systems it might therefore take more than a full minute. There is definitely room for improvement here, especially using multi-threading. - Lack of documentation: There currently exists no documentation for mmt1, nor is the code well commented. If there is interest from others to contribute to mmt1, this will most likely be the first thing I'll fix. On the future development of mmt1: As you can see there is still a lot of work to be done. Most of the features listed above are missing due to time constraints and if there is interest from the community in my proof assistant, then they will be delivered in future versions of mmt1. Hopefully this is just the first of many versions of mmt1. I also hope that I can perhaps inspire some of you to start contributing to mmt1 as well, since we could make a lot faster progress as a team. Perhaps in a few years mmt1 could even become the community proof assistant that people were dreaming of back in 2020 (long before I even discovered metamath). The full tech stack: mmt1 is build using Tauri 2.0. This means that it is a Rust application, which uses the systems web-view for it's UI. Additionally mmt1 uses Svelte 5 as it's JS framework. The full dependency list also includes tailwindcss for styling, monaco editor for the editor, overlayscrollbars for nice looking scrollbars, rayon for mutli-threading, sha2 for hashing and lastly a combination of markup5ever, kuchiki and lightningcss for html/css parsing, validation and sanitation. A note on security: As part of it's theorem explorer and Unicode preview mmt1 renders user input HTML, which always comes with obvious security concerns. To mitigate those, mmt1 checks all HTML against a very restrictive whitelist of tags, attributes and inline styles. If a HTML snippet violates that whitelist, you will be shown a warning and asked to verify the HTML by hand. For more information please see: https://github.com/marloBruder/mmt1/blob/main/guides/security.md I also had another set of questions for you guys: - What do you think the proof assistant should do when the user tries to insert a theorem between two theorems sharing a scope? One option would be to split the scope into two and then insert the theorem in the outermost scope. Another one would be to try to insert it into the scope (if possible) and then have option 1 as a fallback. The last option would be to put a restriction on the database, so that all scopes must have at most one theorem, eliminating the scenario. The downside would be an increased database size, but the big upside would be that all operations such as move, edit and delete would all be much easier to automate. - Would it be OK for you all if my proof assistant is listed on the official metamath website and if yes, what would I have to change to make that happen? If you end up trying mmt1, I would highly appreciate if you could send me your feedback, short or long. What do you like about mmt1? What don't you like? Would you consider using mmt1 as your main proof assistant and if not, why? Lastly, I just wanted to thank everyone that answered one of my questions along the way, I couldn't have created mmt1 without your help :). Best regards, Marlo Bruder -- 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/1cee2a2c-e7fb-48ba-9737-0ae1c77c708cn%40googlegroups.com.
