Latest version of mmj2 (or a better GUI if there is one).

Noam Tene

unread,

Aug 2, 2019, 3:21:09 PM8/2/19

to Metamath

Hi,

I think I can come up with shorter (and more readable) versions for some of the proofs I saw on the MPE explorer.

I will never know until I try it.

I would like to try out mmj2 to experiment with some proofs.

I watched the "Introduction to Metamath & mmj2" video mentioned at "http://us.metamath.org/index.html#faq".

I looked for the "http://us.metamath.org/index.html#downloads" section and I found:

mmj2.zip (7.2 MB) (latest version, 2.4.1 26-Jan-2016, maintained by Mario Carneiro)
mmj2-orig.zip (Mel O'Cat's last official version, 11-Oct-2011)

However, a google search for "mmj2 download" came up with something that looks like a later version at:

https://groups.google.com/forum/#!topic/metamath/3kN15fc2MdY

From watching the video, I noticed that mmj2 is a text based editor.

I do not mind ASCII, I even prefer it in some cases.

At the same time, I find the HTML version much easier to read, follow and present to newcomers who never heard of Metamath.

Are there any HTML or Lyx based editors that incorporate the mmj2 features which I could help beta test?

Thanks,

Noam Tene

Jim Kingdon

unread,

Aug 2, 2019, 5:47:35 PM8/2/19

to Noam Tene, Metamath

Can't speak for anyone else, but for me it was a combination of getting used to the ASCII (at least enough to work with it in mmj2) and using SHOW STATEMENT/ALT_HTML a lot.

Welcome to the project and I'm excited that you have in mind some shortenings which also make things clearer. Those are my favorite kind.

Noam Tene

unread,

Aug 9, 2019, 6:24:30 AM8/9/19

to Metamath

I have made some progress on trying to write my first proof but I am running up against several annoyances that would make many prospective users quit in frustration:

1. The java version of mmj2 that I downloaded keeps crashing or freezing (no response to cancel).
2. There is no autosave so every time it crashes, I lose my work.
3. It is not browser based so it does not work on my tablet. This limits the time I can devote to it.
4. The search feature is cumbersome.
4a. There are 4 windows (cmd, editor, search box, search results) to toggle between.
4b. The search window is too crowded with features that I don't know how to use.
4c. No clear and easy way to copy/paste text from the result window.
5. Searching for ( X + Y ) does not return ( A + B )
5a. I am sure a regular expression could fix that but I could not find examples and I am tired of crashes.
5b. Regular expressions are hard to use when looking for a pattern with nested parentheses.
6. I do not know whether I should look for "( A x. B ) = 0" or for "A x. B = 0" and the search seems to care.
7. Searching for ==> or for && to find implications returns nothing.
8. I could not find something as simple as: "|- -. ps && |- ( ph \/ ps ) ==> |- ph"
8a. Maybe it does not exist in set.mm but I can't tell if it does and that is frustrating.
9. I want to use |- A e. CC ==> |- ( ( 2 x. A = 0 ) <-> A = 0 )
9a. I do not know if it already exists or if I need to prove it myself.
9b. If I have to prove it myself, I'd rather prove: |- A e. CC && |- B e. CC && |- B =/= 0 ==> |- ( ( B x. A = 0 ) <-> A = 0 )
9c. Having it in this form will make my proof shorter but I see a preferece for deduction form in set.mm
9d. Do I need extra proof steps to go back and forth between: "|- 2 =/= 0", "|- -. ( 2 = 0 )" and "|- -. 2 = 0" ?
10. I understand the advantages of deduction form and the desire for shorter proofs but ...
10a. Searching for two possible versions of a theorem is frustrating
10b. Having to write two versions, name them and justify them is daunting.

I am not ready to give up, but any help or suggestions on how to use my time more effectively will be appreciated.

Noam.

Mario Carneiro

unread,

Aug 9, 2019, 8:11:22 AM8/9/19

to metamath

On Fri, Aug 9, 2019 at 6:24 AM Noam Tene <noam...@gmail.com> wrote:

I have made some progress on trying to write my first proof but I am running up against several annoyances that would make many prospective users quit in frustration:

1. The java version of mmj2 that I downloaded keeps crashing or freezing (no response to cancel).

Additional information about this would be helpful. Of course you should use cancel if unify gives you the spinning cursor for more than a fraction of a second and try giving more information, but these are usually bugs and should be replicated and reported.

2. There is no autosave so every time it crashes, I lose my work.

I'm trying to remember what I did about this but I think I would recommend to save often. (I learned to save after a reformat, which I do after every 20 to 30 unifications since unifications tend to cause weird formatting over time) This could be a feature request, but it's not high on my priorities. The crashes are a bigger problem; I don't remember having any issues with completely crashing so I would encourage you to find out what is causing this and report it.

3. It is not browser based so it does not work on my tablet. This limits the time I can devote to it.

This is obviously not something that can be fixed in mmj2. I'm surprised you can write proofs on a tablet though; that sounds like a horrible experience to me even with a great editor.

4. The search feature is cumbersome.
4a. There are 4 windows (cmd, editor, search box, search results) to toggle between.
4b. The search window is too crowded with features that I don't know how to use.

4c. No clear and easy way to copy/paste text from the result window.

5. Searching for ( X + Y ) does not return ( A + B )
5a. I am sure a regular expression could fix that but I could not find examples and I am tired of crashes.
5b. Regular expressions are hard to use when looking for a pattern with nested parentheses.
6. I do not know whether I should look for "( A x. B ) = 0" or for "A x. B = 0" and the search seems to care.
7. Searching for ==> or for && to find implications returns nothing.
8. I could not find something as simple as: "|- -. ps && |- ( ph \/ ps ) ==> |- ph"
8a. Maybe it does not exist in set.mm but I can't tell if it does and that is frustrating.

The search feature in mmj2 is completely experimental. I don't even have the source for it - I decompiled it from the last version of mmj2 released by ocat before he disappeared from the web. I don't use it at all, I keep metamath.exe open just so I can use the search feature there, which is simple and works great. I agree the UI is a nightmare, it is way too visually congested and simple things are not easy. I also keep jedit open to set.mm so I can perform text searches, browse, and edit the file after finishing a proof. I also use it for doing find/replace, because mmj2 doesn't have find/replace.

To search using metamath.exe, I would use something like:

sea * "( ? + ? ) = 0 <->"/j

where "sea" is short for SEARCH and /j is short for /JOIN, which will allow you to search in hypotheses as well.

You can also coerce mmj2 to do a unification search by writing something like:

1:: |- -. ps

2:: |- ( ph \/ ps )

3:1,2: |- ph

(you can also use your particular formulas instead of ph and ps) and unifying to see if line 3 gets populated with a theorem name. This will only find one-step proofs though. It looks like the commuted version of this is available as "mtpor" but I would just use ori and one of the modus tollens theorems, mt3.

Regarding "( A x. B ) = 0" vs "A x. B = 0", yes it matters, only the first of those is syntactically correct and most metamath tools will not recognize the second one. Parentheses in set.mm are not optional - some syntax has it baked in, other syntax does not have it (and forbids it), and using parentheses where not expected is a syntax error. The simple rule is: relations. such as A = B, A e. B, A C_ B, A <_ B do not take parentheses, and operations producing class expressions like ( A + B ), ( A x. B ), ( A u. B ), ( A ` B ) require parentheses. Binary logical operators that take and produce wffs like ( ph /\ ps ), ( ph -> ps ), ( ph \/ ps ) also take parentheses.

9. I want to use |- A e. CC ==> |- ( ( 2 x. A = 0 ) <-> A = 0 )
9a. I do not know if it already exists or if I need to prove it myself.
9b. If I have to prove it myself, I'd rather prove: |- A e. CC && |- B e. CC && |- B =/= 0 ==> |- ( ( B x. A = 0 ) <-> A = 0 )
9c. Having it in this form will make my proof shorter but I see a preferece for deduction form in set.mm
9d. Do I need extra proof steps to go back and forth between: "|- 2 =/= 0", "|- -. ( 2 = 0 )" and "|- -. 2 = 0" ?

Continuing with the parentheses point, the correct syntax for these is:

$e |- A e. CC $p |- ( ( 2 x. A ) = 0 <-> A = 0 )

$e |- A e. CC $e |- B e. CC $e |- B =/= 0 $p |- ( ( B x. A ) = 0 <-> A = 0 )

"|- 2 =/= 0", "|- -. 2 = 0"

The & and ==> notations used on the web site are not actually used anywhere in the metamath specification, so people denote it in a variety of ways. metamath.exe uses the $e / $p style shown here, mmj2 usually puts each assumption on a different line, although possibly the search tool does something different. But the && and ==> notations or whatever they are aren't real syntax, they are display-only, so you can't search for these symbols and expect to find anything.

As for ( ( 2 x. A ) = 0 <-> A = 0 ), I typed sea * "( ? x. ? ) = 0"/j in metamath and it looks like the closest match is mul0or (or mul0ori, mul0ord). To get from there to your statement would also need biorf, neii and 2ne0.

Regarding "|- 2 =/= 0", "|- -. ( 2 = 0 )" and "|- -. 2 = 0", yes you need proof steps to change between these two (note "|- -. ( 2 = 0 )" isn't a thing), but there are a lot of theorems for this so you should usually be able to do it in one step (in this case neii should do the trick).

Using inference form for theorems is seductive, and the insight to use deduction form instead was hard-won. When you assume |- A e. CC, you aren't just saying A is a complex number, you are saying that A is a closed complex number, something you can prove to be complex in an empty context. It turns out that this is almost never what you actually need, and then you are faced with having to refactor all of your theorems after the fact to put the "ph" in. By contrast, if you start in deduction form, then you can easily derive the other forms as corollaries.

10. I understand the advantages of deduction form and the desire for shorter proofs but ...
10a. Searching for two possible versions of a theorem is frustrating
10b. Having to write two versions, name them and justify them is daunting.

If you want to have only one version of a theorem, use deduction form, or theorem form if you don't want the added verbosity of the "ph". Naming them isn't a very hard problem - just tack a "d" on the end if it's in deduction form and "i" if it is in inference form. The algebra theorems specifically have lots of versions because they are commonly used and it is nice to have the right tool for the job. For more advanced things there is usually only one version of the theorem.

You shouldn't really think of the different forms of a theorem as being different theorems, actually. It doesn't add any cognitive load because you can easily predict what one form looks like given any of the other forms, so it's more of a "theorem set" with a single purpose and a single name (the theorem name with the d/i suffix removed). For example, the mul2or theorem:

This is three ways to say the exact same statement. You don't even need to look at the others to guess how they are written. You just pick which version to apply based on whether you have a context or not.

Mario

fl

unread,

Aug 9, 2019, 8:15:23 AM8/9/19

to Metamath

I have made some progress on trying to write my first proof but I am running up against several annoyances that would make many prospective users quit in frustration:
1. The java version of mmj2 that I downloaded keeps crashing or freezing (no response to cancel).

Use Ocat's version.

2. There is no autosave so every time it crashes, I lose my work.

It has always been an issue. Pray to the Lord. Normally it only happens one proof out of 100,

only the very big ones and only when you just finish it.

3. It is not browser based so it does not work on my tablet. This limits the time I can devote to it.

Don't use it on your tablet.

4. The search feature is cumbersome.

Yes. Same answer as for the item #2. To look for theorems the normal way is to use your browser

and a very good editor like Emacs with regexps. That way you will find all what you want.

5. Searching for ( X + Y ) does not return ( A + B )

Use $ . \+ . $ in an editor with a regexp search feature.

6. I do not know whether I should look for "( A x. B ) = 0" or for "A x. B = 0" and the search seems to care.

It does. Infix expressions have always parentheses.

7. Searching for ==> or for && to find implications returns nothing.

Normal. Metacaracters only use in the browser but with no actual symbols in set.mm.

9b. If I have to prove it myself, I'd rather prove: |- A e. CC && |- B e. CC && |- B =/= 0 ==> |- ( ( B x. A = 0 ) <-> A = 0 )

The best way to code something in metamath is:

$p |- ( ( hypotheses ) -> conclusion )

or

$e |- ( ph -> hyp1 )

$e |- ( ph -> hyp2 )

$p |- ( ph -> conclusion )

10a. Searching for two possible versions of a theorem is frustrating

Life is frustrating.

--

FL

Jon P

unread,

Aug 9, 2019, 9:41:48 AM8/9/19

to Metamath

Hi Noam,

I had a very rough time getting accustomed to mmj2 so have a lot of empathy for what you are experiencing. Here is a joke about Metamath, it is known to be quite a rough experience :)

Re crashes I have experienced them quite a lot too. I tend to use ctrl+s between everything I do, pretty much to this level ha ha.

It sounds like you are encountering two of the fundamental transitions to using MM which do take time to get used to:

1. MM works at a super low logical level. It can seem insane at first as any mathematician would obviously accept |- A = ( ( 2 x. B ) + 3 ) -> B = ( ( A - 3 ) / 2 ) as being completely trivial however in MM this is several steps and not an easy thing to prove necessarily. However I would encourage you that it does get easier, once you get used to taking the tiny steps then it becomes more natural, it is a big change though. In my first proof I tried to do 5 steps of algebra thinking that was easy and it ballooned in to over 100 steps of MM and Mario had to come and save me when I was drowning! I would suggest maybe trying the exercises at the top of this thread as they helped me get more comfortable.

2. The hardest long term problem of working in MM is finding things in the database. That takes up maybe 85% of my time when working on a proof, maybe more. It does get easier as you start to get a feel for how the proofs are organised however it can be very frustrating to be continually searching for things (some of which may not exist and some which may be in mathboxes away from the rest of the proofs of that type). It can help to see it more as a treasure hunt where looking around is fun rather than a frustration that the thing you need is hard to find, if that is any use. I like personally to go to the website like here and then use the "nearby theorems" button in the top right to see which ones are similar, that can be really helpful if you find something close but not quite right.

Another thing on this note is to learn the naming conventions, that can really help with looking for things. Like take one of my proofs iocunico, once you know the convention it is obvious that is "ico = an interval with open left end and closed right end" "un = union with" "ico = an interval with closed left end and open right end" so you can basically know what it does without looking. There is more info on naming conventions here.

One final piece of magic is to put an ! before any line you are trying to look up, like !20:: |- 0 e. CC or something. When you do this it will tell mmj2 to automatically try and find a theorem which can justify that step *and*, excitingly, look back in the text to find any steps which you have already done which might help. Learning to use that saved me a huge amount of time and changed proving things from being very painful to just painful, which was a nice step :)

As you can see though there is huge room for improvement of tooling in MM. MMj2 is pretty great and also very rough. We are on the ragged edge of mathematics where there is still a lot of fundamental work to do. The good news is that in 10 years (I believe) every professional mathematician will use a formal proof system so it is exciting to be part of the revolution while it is still in it's early stages.

I hope this is helpful! I would encourage you that the experience you are having is totally normal and that all of us have been through it. If you have any further questions or anything feel free to ask :) Good luck, hope you manage to get over the learning curve as proving stuff can be really awesome and fun.

Jon

Olivier Binda

unread,

Aug 9, 2019, 11:49:35 AM8/9/19

to Metamath

Hello.

I'm currently developping a Metamath based proof-assistant (first for the JVM, then Android/Linux/the browser, later for Windows/Mac... and maybe even IOS, who knows) called Mephistolus.

I have mostly finished the part that handle maths in a human-friendly way and I have just started developing the part that export Mephistolus proofs to metamath proofs.
It'll probably take me a few weeks (or months ?)

Next, I'll work on a proper (flutter) UI and publish a free (Beta) app that allow people to develop (meta)-maths proofs.

So, in a few months, there could be an app that handles all your concerns that you could use on your tablet.

Best regards,
Olivier

Glauco

unread,

Aug 10, 2019, 7:27:22 PM8/10/19

to Metamath

Hi Noam,

I use mmj2 every day, in all my spare time, and it never crashes. And I use it both in Linux and Windows: it's rock solid, for me.

I'm often writing proofs 800+ lines long and mmj2 works with no problem (I'm the real bottleneck). The proof I'm working on today has 1239 lines (I'm actually refactoring it, I will bring it below 600 lines, but even with 1239 lines mmj2 is really fast).

Do you use syntax highlighting? Then mmj2 often crashes. If that's the case, disable syntax highlighting.

Noam Tene wrote:

I have made some progress on trying to write my first proof but I am running up against several annoyances that would make many prospective users quit in frustration:

1. The java version of mmj2 that I downloaded keeps crashing or freezing (no response to cancel).

As I wrote above, I use mmj2 both under Linux and under Win10, and it really never crashes.

4a. There are 4 windows (cmd, editor, search box, search results) to toggle between.

Noam, what do you use cmd for? Editor, search box, search results.... yeah, a lot of alt+tabs to do... I guess that's just the way it is...

4b. The search window is too crowded with features that I don't know how to use.

I use it a lot and I use several of those features, but I admit I don't use all of them (and I wouldn't be surprised if they didn't work as expected).

4c. No clear and easy way to copy/paste text from the result window.

I use mmj2 ver 2.5.2.1021, that's a "fork" with respect to Mario's maintained version (Mel did this forked version some months ago)

It was available here

https://github.com/ocatmetamath/mmj2/tree/ocatmetamath-patch-2

but unfortunately I've now seen it has been removed.

Here you can find some reference to this fork:

https://github.com/digama0/mmj2/issues/12

This forked version allows you to copy/paste text from the result window.

I read a number of projects are in place for new IDEs to be written, but I've always been of the idea that mmj2 is "good enough" to be productive. And there are a few (apparently easy) features that could be implemented, and those would make mmj2 even better.

In Mario's answer to your post, I read that he doesn't have the source for the search feature: this could be one of the reason why nobody works on improving mmj2 instead of writing an IDE from scratch (or a plugin for other IDEs, that would mean more dependencies).