metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

[David A. Wheeler]

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

[Thierry Arnoux]

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

[Alexander van der Vekens]

I just had a look at metamath-lamp itself and at the video. It is actually very impressive, but, to be honest, I have no idea how to use it. There is an urgent need for instructions, a user guide, a tutorial, etc. before it can be  recommened for beginners...

[David A. Wheeler]

> On May 26, 2023, at 4:19 PM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>
> I just had a look at metamath-lamp itself and at the video. It is actually very impressive, but, to be honest, I have no idea how to use it. There is an urgent need for instructions, a user guide, a tutorial, etc. before it can be recommened for beginners...

*Absolutely* 100% agreed!! As I said:

> A problem for metamath-lamp is the lack of instruction showing how to *use* it.

> ... But it wouldn't take much to create

> a basic help document & a few videos to help people get started.

Ask and ye shall receive!! As of this morning the first draft of the
metamath-lamp guide is available here:
https://github.com/expln/metamath-lamp/blob/master/docs/guide.md

I intend to add more to it. I think it needs at least 3 worked examples of proofs,
with more desirable. It currently shows how to prove 2+2=4, and that should help.

--- David A. Wheeler

[Alexander van der Vekens]

OK I tried it again using

On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote:

Ask and ye shall receive!! As of this morning the first draft of the
metamath-lamp guide is available here:
https://github.com/expln/metamath-lamp/blob/master/docs/guide.md

I wanted to proof ( 5 + 7 ) = ; 1 2. At the beginning, metamath-lamp did not give any helpful hint by itsself (you have to know some basic metamath theorems in advance), and often the prove action took very long (several minutes), even after I gave the hint that "6p5lem" can be used.

In between, I was stuck when trying to prove ( 5 + 7 ) = ( ; 0 5 + ; 0 7 ) - I am not able to apply oveq12i to continue with using dec0h to complete this proof (step).

The replacement of a temporary variable is a little bit cumberson: if you want to replace &C1 by 6, you cannot change it at one place (and then it is replaced everywhere, as in mmj2), but you have to click A (apply a substitution to all statements), then enter &C1 and 6 manually.

In the following, a second line with 5 e. NN0 was created (with the massage This statement is the same as the previous one - '2' ) - at first, it was not possible to get rid of it, I succeded, however, after a while...

At the end, I needed about one hour to finish the proof successfully (with metamath.exe it was done within a few minutes).

To summarize, I think metamath-lamp is not stable/intuitive enough to be suitable for a beginner at the moment.

Finally, it would be very helpful if screen shots were available in this user guide.

 

[David A. Wheeler]

> On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote:
>
> Ask and ye shall receive!! As of this morning the first draft of the
> metamath-lamp guide is available here:
> https://github.com/expln/metamath-lamp/blob/master/docs/guide.md

> On May 27, 2023, at 10:17 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
> I wanted to proof ( 5 + 7 ) = ; 1 2.

Ouch, that's a worst case goal for metamath-lamp when compared to mmj2.
The mmj2 tool has automations *specifically* for simple calculations like this,
while metamath-lamp does not. But it's a valid goal, so carry on!

> The replacement of a temporary variable is a little bit cumberson: if you want to replace &C1 by 6, you cannot change it at one place (and then it is replaced everywhere, as in mmj2), but you have to click A (apply a substitution to all statements), then enter &C1 and 6 manually.

In mmj2 you still need to manually replace the work variable (&C1) by its replacement somewhere (6).
The current assumption in metamath-lamp is that for substitutions you'll always use the replacement command instead.

That said, I think you're right, it would be better if metamath-lamp also allowed people to
just edit a work variable into an expression and have unify automatically do the replacement.
I've added that as a proposal here:

https://github.com/expln/metamath-lamp/issues/43

> In the following, a second line with 5 e. NN0 was created (with the massage This statement is the same as the previous one - '2' ) - at first, it was not possible to get rid of it, I succeded, however, after a while...

You should be able to select the statement & then choose "delete". If that didn't work, I'd love to know why.

> At the end, I needed about one hour to finish the proof successfully (with metamath.exe it was done within a few minutes).
> To summarize, I think metamath-lamp is not stable/intuitive enough to be suitable for a beginner at the moment.
>
> Finally, it would be very helpful if screen shots were available in this user guide.

Good point. In the long term I intend to create a video, just like I did with mmj2,
but screen shots are still a good idea.

Thanks for the feedback! I think you're right that metamath-lamp needs improvements
in its UI & capabilities. However, I think some of that suggests a need to improve its documentation
to clarify how to use it; mmj2 also has some oddities that work fine once you know what they are.
I'm going to work on improving its documentation to hopefully make it easier.

I still think it is helpful to have at least one tool that work "without an install" and can
immediately work on smartphones.
mmj2's automations and some specific mechanisms give it power that metamath-lamp
currently lacks, but some people may be unwilling to go through the effort of installing a tool
just to try it out. I'm hoping that metamath-lamp can be, at the least, a way
to entice people into trying to create metamath proofs themselves.

--- David A. Wheeler

[Igor Ieskov]

>>> you have to know some basic metamath theorems in advance

My goal is exactly opposite :) That's why I designed the interface this way when justifications are not shown by default and users see only statements and if they are proved or not. Apparently this goal is not fully achieved so far due to lack of automation, documentation and examples. But even now it is possible to create proofs without knowing any of the metamath theorems. I even recently provided such a proof (created myself without knowing metamath theorems) as a response here https://groups.google.com/g/metamath/c/f35gd8Cxozo/m/UIwARA0NAQAJ  (and I am planning to implement an interface when justifications are easily accessible too :) )

>>> and often the prove action took very long (several minutes), even after I gave the hint that "6p5lem" can be used.

Usually, when metamath-lamp is given a hint what assertion to use, and other parameters by default, it should work fast enough. Could you please check if you have "parentheses" setting set correctly? In order to do this:
1. Load the database which you encountered this issue with.
2. Go to Settings tab.
3. Click "refresh" button next to the "Parentheses" setting. This will launch a process which will determine what constants are used as parentheses in the loaded database.
4. Click "apply changes" on the Settings tab to save updated parentheses and check if the issue with slow proofs is resolved or not.

Parentheses comparison lies in the core of unification algorithm metamath-lamp uses. That's why it may affect performance. If the above doesn't help then I would appreciate if you create an issue in metamath-lamp repository. (please see how to submit an issue at the end of this post)

>>> you have to click A (apply a substitution to all statements), then enter &C1 and 6 manually.

There is a more convenient way to do this which became available only recently. You can use sub-expression selections. This way you can substitute even two or more variables at once. This is demonstrated at 3:40 in this video (no sound) https://drive.google.com/file/d/1IwdHLpQreZ_1CJFZJmptRJc2unO8aNh4/view?t=220 

>>> In the following, a second line with 5 e. NN0 was created (with the massage This statement is the same as the previous one - '2' ) - at first, it was not possible to get rid of it, I succeded, however, after a while...

This kind of error messages is going to appear very often in metamath-lamp. Here is the preferred way of fixing it:
1) Select the statement this error message appeared for by clicking the checkbox left to the statement. This must be the statement right above the error message. And make sure this is the only statement selected.
2) Click "Merge two similar statements" button. This button looks like two lines merging into a single line (like Y).
3) A dialog should appear where you will have possibility to select what statement you want to continue using. (you selected one statement,  metamath-lamp finds another duplicated statement automatically)
This way one of the duplicated statements will be removed automatically and metamath-lamp will update all the justifications which used the removed statement so they will use the statement you chose to continue using.
Also I am planning to automate handling of this kind of situations so in the future it will require less manual work.

>>> I think metamath-lamp is not stable

If you saw any other kind of errors (like errors in the console of a browser), I would appreciate if you submit an issue. If by instability you mean varying speed of work of metamath-lamp, then yes, that might be an issue and I cannot do much about it at the moment, but I will think on how to improve this. Thanks for letting me know this.

Thank you for spending your time and providing this feedback. It is very useful for me to understand how others are using this tool and what kind of issues arise.


In order to submit an issue in metamath-lamp repository please do the following:
1) Create an issue here https://github.com/expln/metamath-lamp/issues , give it a short name and provide some description of what is not working as you expected.
2) If possible, provide steps to reproduce. I expect it to be not too difficult usually:
a) Use "export to JSON" action (located in the top right corner menu on the editor tab) to save json representation of the assistant state at the moment when you are about to reproduce the issue. Attach this json to the issue.
b) Specify what next step(s) lead to the issue.
3) Specify the browser name and its version where you face this issue.

-

Igor

[Alexander van der Vekens]

Hi Igor, hi David,

I think the current status of metamath-lamp is already very good, but not good enough for a beginner. So there is room for some improvements (especially regarding documentation, as indicated by David).

In any case, it is a good candidate to replace the Metamath Solitaire Applet (does it actually work somewhere/somehow?) very soon. Maybe a restriction of the scope (for beginners) could help: if only propositional or predicate calculus (or ZF set theory) is used (this is a great functionality of methamath-lamp to restrict the amount of set.mm to be loaded and used. "Stop at exists2" would only load definitions and theorems for propositional or predicate calculus, "Stop at hsmex3" for ZF set theory), metamath-lamp may be fast and intuitive enough for a beginner.

[Igor Ieskov]

I want to add few more things to consider before suggesting metamath-lamp as a proof assistant to start with in the first place. Not that I don't want a tool I am developing to be present on the front page of the official Metamath site :) But I think I have to mention what may be not so obvious from the technical point of view:

This is a pretty new tool, I tested it on only simple proofs and use cases.  So far it worked well for me.   I do my best to cover complex functions with unit and integration tests. But without "testing in the field" I cannot assure that there are no bugs. And this is not a java application when if it works on developer's computer then most probably it will work on many other computers. It is JavaScript code running in a browser and risks of something may go wrong for other users is higher than in the case of a typical java application, for example.

metamath-lamp runs completely in a browser so I will not know how often and how successfully it is used by others. Therefore there is a risk that official Metamath site suggests a tool which performs not so good as it has to and nobody knows that.

-

Igor

[Mario Carneiro]

> Therefore there is a risk that official Metamath site suggests a tool which performs not so good as it has to and nobody knows that.

I don't think this is a major concern, as long as we manage expectations on the landing page. Metamath and all associated tools come with no warranty, after all. I see no reason to wait for it to be perfect before making it available for use, since anything is better than nothing and users can always download another proof assistant if they decide the JS version isn't great. (And BTW: this is the case almost every time I have seen a "we put our theorem prover on the web" situation, the web prover is not actually all that great and if you want to do "real work" you will eventually want to download the tool and use it locally. But at that point the web version has already satisfied its purpose as a gateway to heavier use. This is not to say that you can't make the web prover as good or better than the offline competitors, although even with a perfect implementation there are some fundamental limitations regarding how files are read and written in a web browser that make it not quite as good as native due to the sandboxing.)

--
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 on the web visit https://groups.google.com/d/msgid/metamath/8f557136-b1cc-4b7f-add7-1f0ed4275280n%40googlegroups.com.