Hi David, Good idea!
I think we should also list Yamma: https://marketplace.visualstudio.com/items?itemName=glacode.yamma I've been using it recently to write my latest proofs, and it is quite functional. BR, _ Thierry On 24/05/2023 03:24, David A. Wheeler wrote:
I've been experimenting with the proof assistant metamath-lamp, including abusing poor Igor with a variety of suggestions :-). In short: I'm quite impressed with metamath-lamp. Of the functions that I routinely *use* in mmj2, the only one that I really miss is mmj2's automation routines. I'm sure automation could be added to metamath-lamp (it's not a lot of mmj2). What's more, metamath-lamp is quite useful even without them. It has a few minor issues due to its newness, but there's a lot to like. More importantly, metamath-lamp brings something new & *VERY* valuable: It can be used without installing *anything*. That makes it an *extremely* helpful tool for people who might be interested in trying to develop metamath proofs, because it eliminates that startup time. Metamath-lamp even works well on a good smartphone (it currently has a minor UI problem due to the lack of an "alt/opt" key, but that is easy to fix). Even if someone switches tools later, metamath-lamp is a great "gateway drug" :-). I would encourage others to check out metamath-lamp: * Source code Repo:<https://github.com/expln/metamath-lamp>. * Use it:<https://expln.github.io/lamp/latest/index.html> * Video demo (no audio):https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?usp=sharing A problem for metamath-lamp is the lack of instruction showing how to *use* it. metamath-lamp has a number of tooltips, but it's easy to not notice them. It also has no help file or document, and the only demo video has no sound. In contrast, mmj2 comes with a nice long hands-on tutorial, and I created a Youtube video that walks through that whole tutorial. But it wouldn't take much to create a basic help document & a few videos to help people get started. We currently have a "Q: Where do I start?" on the metamath.org front page that ends with this: ~~~~ You can experiment with simple proofs in the Metamath Solitaire applet. To actually create real metamath proofs, you'll want to download a tool. A common tool is mmj2. David A. Wheeler produced an introductory video, "Introduction to Metamath & mmj2" [retrieved 4-Aug-2016]. ~~~~ I would like to modify this text to help welcome people in, but also note at least metamath-lamp, and probably other tools as well. I propose changing it to something like this (at least once better tutorials are available): ~~~~ To create real metamath proofs, you'll want to download a tool. We suggest trying one of these tools for creating metamath proofs: * metamath-lamp. This is an easy-to-use web-based GUI proof assistant. You don't need to install anything - just use your browser. To learn how to use it, see [video not appearing in this film]. Go *here* to start using it. * mmj2. This is a GUI proof assistant written in Java, so you must install it as well as a Java Virtual Machine (JVM) to run it. This is probably the most common tool currently in use for creating metamath proofs. It includes some automation to automatically complete some proofs. David A. Wheeler produced an introductory video, "Introduction to Metamath & mmj2" [retrieved 4-Aug-2016]. * metamath-exe. This is the original tool, written in C, for supporting the metamath formal system. This is a text command line tool for supporting metamath and includes a proof assistant. See the [metamath book] for more information on how to use it. The name of the command is "metamath", but we often call it "metamath-exe" to distinguish this program from other programs and the underlying Metamath system. If you do not like using GUIs or you have specialized needs, this might be the proof tool for you. Once you learn how to use one tool, it's very easy to learn how to use another, so we encourage you to "just start" with any one. ~~~~ I'm sure it could be worded better, and maybe we should list other tools or link to a longer list of Metamath proof assistants. The point is to help people get started - I'd love to see even more people join in the fun of creating and improving Metamath proofs. I didn't list some other proof assistants because it was my understanding they're inactive: * mmpp<https://github.com/giomasce/mmpp> * Igor<https://github.com/Drahflow/Igor> Metamath Zero is a different beast, so I didn't list it either. We probably need to fix up the "tools" list page, and link to that:<https://us.metamath.org/other.html>. But I think showing new users a huge list is overwhelming. --- David A. Wheeler
-- 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 on the web visit https://groups.google.com/d/msgid/metamath/65bba079-0ae6-aa7c-76e9-457b63cb580b%40gmx.net.
