The top regions, namely, the "Loaded: ..." area, the "Settings/Editor" tab selection bar, and the Editor icon bar have too much space (especially when the Editor icon bar overflows into multiple lines). Also, on narrow screens the icon bar overflows into multiple lines.

This is a big problem on smartphones because their built-in displays have so few pixels. It still works, but if these fixed regions took less space, there'd be a lot more room to play with :-).

This isn't as big a deal on laptops, but even there, most displays are wide but have limited vertical space.

At the least, tweaking the CSS to reduce the vertical padding would probably give at least another line back.

Even more interesting would be tweaking the icon bar so that if there isn't enough room some less-used icons would flow into an overflow menu (the "3 dots" icon). On smartphones in particular that would be really nice - it works without, but that would definitely improve things.

I propose adding a third source input type, "inline text". It just lets you put text into a text box, that would then be read. This text would also be included as part of the JSON or URL.

This would make it easy to create a proof that builds on an existing database and other proofs not in the database, by letting you temporarily add those proofs to what you're working on.

The guide should eventually have several worked examples so that people can learn from them.

The reccot example from here:
https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view?t=150
should eventually be added as one of those worked example.

NB: It'd be better if it started loading "up to but not including" reccot. That is much easier to explain, and works no matter how set.mm is reorganized.

In the 2p2e4 example, around this text:

and press Enter (Return).
Unselect the "qed" statement.
As an experiment, select Unify with no statement selected;
you'll see that in this case nothing happens.

Use duplication instead of add, as suggested here in #28 :

Looks like on this step we also could use duplication and small adjustment of the new statement. Probably this is the reason why I have not noticed existence of the issue with selecting/unselecting the last statement - because I used duplication in many cases.

The metamath-lamp UI includes many uses of alt+left click. This action is not possible on typical smartphones to my knowledge. As far as I can tell this is the only UI mechanism that makes it not possible to fully use metamath-lamp on smartphones. In particular, you currently can't change a provable statement into a hypothesis if you can't use alt+left click. (Yes, you could create a JSON file and load it in, but that's a terrible workaround.) You also can't use the statement selector on smartphones, which is unfortunate because it's the device where keyboard use is the most annoying. Finally, sometimes alt+left click is inconvenient even when you're using a laptop/desktop.

I would really like to see a "long click" interpreted as alt+left click. That is, it would be considered alt+left click if the user presses the touchscreen or left button down, holds it down for a long time (say at least 1500 milliseconds) on the same element, and then it's released without moving off the selected element. That one addition would be enough to use everything on a smartphone, and isn't hard to understand.

I earlier noted this in #28, but after thinking about it, I've decided that I would really like this feature.

As far as I know React doesn't directly support longpress, but it doesn't appear to be hard to implement. Here's a discussion and sample code:
https://stackoverflow.com/questions/48048957/react-long-press-event

The "time for long press" could be a configurable setting in Settings. I'm guessing 1500 milliseconds would be a good default.

Note: this means a left-click on a not-being-edited proof statement would edit, but a long-click on a not-being-edited proof statement would invoke the statement selector. I don't think that will cause any problems, because both left-click and long-click only happen on touch/mouse press up. In short, the system can easily tell the difference; it's an alt-click if if the mouse button was held down on the element for at least "time for long press" time.

Ideally there'd be a visual indicator when the press-down-time had been exceeded that could be seen by a smartphone user. So I don't think it can be just a cursor image change (which would be nice but the user's digit would hide that). It could be a screen flash (e.g., briefly set the background to another color) or some other simple visual indicator; just pick something easy and distinct. That said, adding the visual indicator could be done later. My concern currently is to just have something that works.

This is a relatively high priority for me, because it suddenly means everything works on a smartphone. That doesn't make it necessarily a high priority for you, but I figure I can beg :-).

In general we want to generate compressed proofs. However, if you're trying to show "how metamath works", showing uncompressed proofs can help illuminate a lot of things that aren't otherwise obvious. Thus, from a teaching point of view it could be helpful to be able to select a flag that would then show uncompressed proofs, as a way to fully reveal the mechanisms.

The editor has to provide possibility to return to one of few previous states. The number of kept previous states may be not too big, due to limitations of browsers.

Known workaround:
If you know that the next action may produce unwanted results, you may use "export to json" to save editor state before that action. "export to json" feature is available in the top right corner menu on the editor tab. You also may include current timestamp to the json text before copying. This will help to navigate between such stored states if you have many of them stored in a file. In order to restore a state, use "import from json" feature available in the same menu. Don't put the timestamp when restoring, if you saved it previously, only json data should be put into the "import from json" dialog. This is a temporary solution until undo/redo is implemented.

Currently when you edit and you press "left parenthesis", the tool adds "right parenthesis". This makes sense in some contexts, but it's annoying in others - in many cases you are certain to need to delete the right parenthesis, and their insertion is more trouble than help.

I think using them should be an editor setting (on/off), so if you hate them they stop getting added.

If it's on, it'd be nice if they were inserted using a smarter algorithm. Here's a simple one (algorithm 1):

Insert the matching closing "paren" after the opening if the expression is at the end or the expression is followed by a closing "paren-like" symbol.

Algorithm 1 is at least simple to simple to implement.

Another algorithm (algorithm 2) would be:

only add the right paren after the left one if the whole statement would be syntactically valid (once the "(...)" expression was completed).

However, this second one is complicated, I'm not sure how to do that quickly & I doubt it's worth the trouble.

The tool currently lets you download set.mm from the web. I propose adding iset.mm (latest) as well. The iset database has multiple developers.

There's already a "copy" button in the edit selector dialogue. It'd be really convenient if there was also a "paste" button that did the equivalent of control-V / command-V; it would be sensibly placed next to copy. It should work even if you're not currently in edit mode (basically it'd do the equivalent of push edit button, control-V, Return).

The bottom-up proof mechanism is quite useful, but slow. I believe it starts here: src/metamath/mm-utils/MM_provers.res.

There will always be limits to it, but I suspect it can be sped up:

1. Run matches in parallel. This might significantly speed things up, since this is compute bound and (mostly) embarassingly parallel. However, I fear it'd take a non-trivial amount of code to do. Parallel.js might help do this (especially if the loaded database can be passed as a read-only global environment), which builds on the web worker API. Some JavaScript parallel mechanisms requires copies of large data in each thread; that would require a copy of the expanded database in each one; that would use up fast amounts of memory, so only a few threads could be run in parallel. But it looks like there are ways to share read-only data, and I think that's all you need for the big data structures.
2. Quickly identify & discard things that can't match. IIRC, metamath-exe and mmj2 also do bottom-up searches, and they use some heuristics to quickly identify "can't match" cases before doing a full unification.

Regarding number 2...

Metamath-exe source file mmunif.chas some optimizations to skip impossible unifications. It precomputes some values, and then uses them to skip some options. It says:

  /* Quick scan to reject some impossible unifications: If the
     first symbol in a substitution is a constant, it must match
     the 2nd constant of some earlier $a statement (e.g. "<" matches
     "class <", "Ord (/)" matches "class Ord A").  Same applies to
     last symbol. */
  /* This prefilter is too aggressive when empty substitutions
     are allowed.  Therefore added "g_minSubstLen > 0" to fix miu.mm theorem1
     Proof Assistant failure reported by Josh Purinton. */

Similarly, its file mmpfas.c has some ideas that might be useful:

  /* Speedup:  if first or last tokens in instance and scheme are constants,
     they must match */
  if (firstSymbol) { /* First symbol in mString is a constant */
    if (firstSymbol != stmtMathPtr[0]) {
      if (g_MathToken[stmtMathPtr[0]].tokenType == (char)con_) return 0;
    }
  }       
        
  schemeLen = nmbrLen(stmtMathPtr);
            
  /* ...Continuation of speedup */
  if (secondSymbol) { /* Second symbol in mString is a constant */
    if (schemeLen > 1) {
      if (secondSymbol != stmtMathPtr[1]) {
        /* Second symbol should be tested only if 1st symbol is a constant */
        if (g_MathToken[stmtMathPtr[0]].tokenType == (char)con_) {
          if (g_MathToken[stmtMathPtr[1]].tokenType == (char)con_)
              return 0;
        }
      }
    }                                      
  }
  if (lastSymbol) { /* Last symbol in mString is a constant */
    if (lastSymbol != stmtMathPtr[schemeLen - 1]) {
      if (g_MathToken[stmtMathPtr[schemeLen - 1]].tokenType ==
         (char)con_) return 0;
    }
  }     
        
  /* Speedup:  make sure all constants in scheme are in instance (i.e.
     mString) */

There's no rush for this, since it clearly works. But I thought I'd record this idea now.

Metamath-lamp is surprisingly functional on smartphones. However, there is no "alt-left click" on typical smartphones. I propose adding some mechanism so that users who can't (easily) do alt-left click can still access all of metamath-lamp's functionality.

I propose adding two more buttons on the toolbar:

• "S" - Select statement fragments. When this is selected, the cursor changes, and you can pick a statement, which immediately opens like alt-left click & lets you keep selecting statement fragments. Use circled X, or this "S" again, to leave the mode.
• "H" - "Hypothesis Toggle" - Only works when 1+ statements are selected; those statements are toggled between "hypothesis" or not.

Feel free to implement it some better way. At the least, being able to create hypotheses is key for creating proofs on smartphones, but simplifying statement fragment handling is also very nice on smartphones.

The only other issue on smartphones that I found is that smartphone touchscreens don't have "hover". To address that, see #23. In short, long-downpress could also show the hover text (but make sure the pressing finger doesn't cover the text!).

There should be an option to include more technical info into json obtained by "Export to json" action. This info could be then send in an issue report.

Example of the technical info:

1. browser version
2. current set of settings
3. how long metamath-lamp has been working since the page load
4. amount of currently used RAM (if it is possible to determine from JS)

There should be a clear explanation why users may want to include this info into the exported json. Also there should be possibility to specify what kind of info users don't want to include.

mmj2 users learn to repeatedly press "control-U" to unify.

Metamth-lamp should also interpret control-U as a request to run unify (as if the unify icon had been pressed), as it's likely from someone who's used mmj2. The tooltip should mention this shortcut, e.g., as (control+U).

It's not immediately obvious to a new user how to get a completed proof once you have one.

Currently you need to "unify" all, then select the checkmark on qed. That's not obvious, and that action should be obvious.

Perhaps next to "unify" could be a "Generate compressed proof" button. It would try to unify all the statements (if that hasn't already been done), and then if qed can be proved, do the equivalent of selecting the checkmark next to qed. That would make it obvious, and also it's easier to select.

Also, perhaps when a proof of "qed" is first completely proved (back to all leaves), there can be a statement like "Congratulations, you've proved the conclusion. Select 'Generate compressed proof' or the checkmark next to the qed statement". That would make it more discoverable, and as well as being a delightful message to see.

@icecream17 noted confusion with terms like "top-down" in #28. Maybe we should use teems like "forward towards goal" and "backwards from goal'".

Please set the GitHub description so that others will know what this program is. Other systems use the "description" field to find programs, explain them, etc.

I suggest this description (edit to taste!):

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

When viewing the main front page https://github.com/expln/metamath-lamp look near the top right for a "gear". Click it and it will let you edit the description field (it's currently empty). Thanks!

The "ESC" key is often used as a mild undo - it'd be nice if it did that in more cases, especially for new users. In particular, it'd be nice if metamath-lamp remembered the last action, and then implemented ESC as follows:

• If the last action clicked on a "P" to reveal the justification, an "ESC" should re-hide the justification. Part of the problem is that while there's a trash can to eliminate the justification, there's no obvious visual indication of how to re-hide the justification (press "P" again). It might also be nice if there was a "close" icon near the trash can, if you want to close (hide) the justification instead of deleting it... but make sure those 2 icons are clearly different & what they mean :-).
• If the last action opened the H/P dialogue (using alt-left click on P), ESC should close the dialogue & keep the current state unchanged.
• If the last action opened the statement select sub-toolbar, ESC should close that sub-toolbar.
• If the last action selected a statement, ESC should unselect it.
• In general, in any dialogue (modal) box, ESC should leave (the equivalent of Cancel).

It'd be good if there was a link that automatically opened a new tab to the guide (and maybe to the metamath-lamp home page). That way, users could quickly get more information without hunting.

It's be nice if it was possible to use metamath-lamp without a keyboard.

One approach:

• Any use of arrow keys switches to a keyboard use, and highlights one of the control points
• Arrow keys (up/down/left/right) move that direction to the next control
• Tab/Shift-Tab move like left/right
• Space or Enter acts like left click.
• Alt-Space acts like alt+left click
• ESC continues to escape many things

It'd also be helpful if many of the icons had keyboard shortcuts, e.g., control+U invoked unify, "+" invoked the nearest "add"

Using a mouse button or touch leaves this mode.

By default searches, unifications that add statements, and bottom-up proofs should skip any statement (an axiom or theorem) with a comment that includes the text "(New usage is discouraged.)". This should be a checkbox in "Settings":

(Checkbox) Ignore statements marked with "(New usage is discouraged.)"
(default checked).

If a user hand-adds such statements (say in a justification or as a root of a bottom-up search) then that's fine, and it shouldn't remove them. The point is that the tool should not be automatically adding or reporting them by default.

As mentioned here #50 (comment) there are pros and cons of keeping the guide in a separate repo. But number and significance of pros is greater than cons, so I think it is better to move the guide to a new repo. I am not against "lamp-guide" name.

Pros:

a separate repo would indeed focus each repo

The big advantage of putting it in the Metamath org is that if someone dies, it's easy to continue. Of course, please don't die soon on us :-).

XD XD XD

one advantage of a separate repo, in the metamath org, is that it'd get more visibility and maybe more would help improve it. That's a decent argument for doing it.

Cons:

A problem with this approach is that this separation often leads to skew, that is, the documentation and code increasingly diverge because code changes don't naturally lead to documentation.

This should not be a big problem. Each version of metamath-lamp has its unique URL. We can specify in the guide which version it describes. I will try to update the guide as soon as I release a new version. We should keep guides for all the previous versions so it should be easy to select a version of mm-lamp and the corresponding guide to read it without being annoyed by significant discrepancies.

Background: I've experimented using metamath-lamp on my smartphone. It was surprisingly good!! Reasoning backwards took longer, but it's still useful. However, because touchscreen devices (like smartphones) don't have "hover", users of touchscreens can't see the tooltips. The lack of tooltips really hurts discoverability on the smartphone, which is too bad since otherwise the experience is generally pretty good.

So I think the code should be tweaked so that tooltips show on "regular" computers and on smartphones. For example, the tooltip should show on a long downpress (smartphone) or hover. A down+up (click) should activate whatever it is.

Here's some information on how to configure tooltips like this:

https://stackoverflow.com/questions/69030402/material-ui-tooltip-is-not-working-on-mobile

This isn't the only issue on smartphone, as I don't know of a way to distinguish left-button from Alt+left-button. That might need to be fixed separately.. but making tooltips work should at least be easy :-).

Currently visualization is a global setting, which is less flexible.

Instead, when a justification is shown, add a dialogue to the right to enable or disable visualization of that justification. Then you can enable visualizations of some justifications and not others. Also, it makes the option visible "when you might use it" - the visualizations only make sense when you're showing a justification.

You might have a setting to set the default value of a visualization, that is, when you show a justification, should it be visualized or not by default? That would have a similar effect, but would also be more flexible.

I think it'd be helpful to allow people to easily preload an existing proof into the prover. Obviously that's not necessary to create a new proof, but there are useful reasons for it:

1. You're new to Metamath & want to see what an existing proof looks like in the tool.
2. You'd like to see the visualizations on an existing proof. The visualizations are really cool, esp. for those new to Metamath.
3. You might want to create a proof that's similar to an existing proof.

If there are already existing statements, there should be a dialogue like "This will erase and replace your existing work. Are you sure you want to do this (y/N)?"

Current way of merging of duplicated statements involves some manual work. In many cases it could be automated. Currently the process of merging is as follows:

1. Select the statement this error message "This statement is the same as the previous one - 'label'" 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.

Here's a crazy idea.

Perhaps metamath-lamp could allow people to reverse the statement list (e.g., the "basics" first). It's a weird idea perhaps, but I'm pretty confident that it's much easier for LLMs to start with the conclusion and generate the other parts than the reverse. I hope to eventually do some work with the AI, as a way to give hints about what to try next, and it might be nice if it'd be possible for metamath-lamp to show the statements in the same order.

If you think it's crazy, never mind :-). But I thought I'd raise it as an idea.

A default MacOS keyboard doesn't have an "Alt" key, it has an "Opt" key that does the same thing.
I think it'd be clearer to new users if the "Settings" display made it clear, near the
"Edit statements by" entry, something like the following:

On some keyboards 'Alt' is labelled as 'Opt'

I don't think you need to change the menu entries everywhere, as long as the user
gets appropriate hints that the same key has multiple names.
I'm not sure that all MacOS keyboards don't have an "Alt" key, which is why I'm suggesting
this specific wording to cover all bases.

This is a UI proposal, it doesn't change functionality. Do with it as you will, it's not critical, but maybe you'll find it interesting.

Currently there's a little "P" that toggles display of a justification on the next line. But often I want to see all justifications or none, and having each one on its line wastes a tremendous amount of space when I'm using a larger display.

I proposal instead having a toggle at the top that turns on/off displays of justifications; when on, it displays in the same line the justification or something that indicates it's a hypotheses (maybe HYP). When off, this becomes a tiny minimized column that shows H or P (if it's a justified provable statement) or "-" (if it's supposed to be provable but is not yet justified). Hovering over it shows a tooltip: "Hypothesis NUMBER" if a hypothesis, the justification if it's justified along with "Press Alt- to generate proof", or "This is not yet proven". You could change a statement between H and P by selecting it and then selecting a new button at the top "H<>P" (this would make the ability to change a statement type more obvious).

The "proving bottom-up" dialogue box options can be a little confusing. Here are suggestions, based on what I think it's doing. If my understanding is wrong, please change the text to make these confusions less likely in the future :-).

Change "Root statements" to "Required statements". I think the point is to tell metamath-lamp that it must use these statements. "Root" is confusing here.

Change "Label" to "Label of root justification" or "Root label" or something like that. Yes, it's a label, but what does the label select? It's the initial justification or root justification or something like that.

I think that "length restriction" controls how "Search depth" is interpreted, but that's not obvious. It should be more obvious that "length restriction" and "search depth" are related, and that they're not related to the "label" on the same line. If that's the right interpretation, I'd put a spacer before this pair (so it's clearly not related to "label"), and reverse their order like this:

• Search depth restriction: "<", "<=", "Unrestricted"
• Search depth: (Number) - grey this out when "Unrestricted" is selected and show "N/A"

I'm not sure this is worth it, but here's an idea anyway :-).

It might be neat to have a display mode option where statements are shown in a "pretty" form when they're not being edited. By "pretty" I mean "use the althtmldef entries for each symbol". This would look nice & certainly make some screenshots compelling :-).

If the statement selector can work on these pretty displays, and adding support for "paste" on a selected statement is added per #42 , then people can easily copy and paste statement fragments in this pretty format, which would be nice!

There is the risk that a malicious database could include some malicious HTML. The simple solution would be to only allow a short list of tags and attributes. Something like this:

Allowed tags: sub sup span i b u small font
Allowed attributes: size class style="color:..." face

Obviously these can be tweaked if something is missing.

I'm not sure if this is worth doing, but I thought I'd record the idea.

The "description" field edits don't work like anything else, and that inconsistency is jarring. It should support left-click to edit, alt+left click to select like everything else. UIs are more complicated when there are inconsistencies.

Currently you can select a statement, then use arrows to move it up & down. That works, but dragging & dropping would seem more intuitive. If you select something, then drag it up or down beyond another statement, it seems like that should also work. It'd be okay if the drag area was limited the left-hand area (e.g., selectors), to avoid confusion with selecting parts of statements (e.g., to copy them).

It happens very often that I get an error related to labels when adding new hypotheses. This is due to more strict rules for hypothesis labels. This should be automated to reduce necessity for a user to modify hypothesis labels manually. If possible, respecting set.mm naming convention.

Search is easy to use, but it's hard to be specific because it allows 0+ symbols between each symbol.

It'd be nice to have an option (irrelevant in regex) to require that "symbols must be adjacent". If enabled, the pattern specifies a sequence of symbols that must be adjacent (though they could be inside a matching statement). Obviously this is only useful once the search pattern can search on variables (since otherwise there are few useful working patterns).

As a bonus you might add symbols that re-add flexibility. E.g., $$ for one symbol, $+ for 1 or more unspecified symbols, and $*for 0 or more symbols. But that could be done later or never. I'm not sure what the right specifiers should be in this case, and that extra flexibility would require backtracking (or using a DFA which would be complete overkill in this case).

After playing with metamath-lamp, I think there are some simple ways that the UI could be easier to use by making "qed" special. All proofs have some final goal, here called "qed":

• If a statement is saved and there are no other statements, automatically label it as qed.
• Before and after doing any unification (and maybe other actions like adding a step), if there's a qed step, automatically move it the last step in the list.

The idea is to move "qed" to the end automatically, otherwise it can end up in weird places.

Once you're done with a proof, it's not clear how to restart from scratch. You can select and delete all the statements, but that doesn't load a different database. It'd be nice to have a "reset" button, which of course would ask for confirmation (default NO) before erasing everything.

When pressing alt+left click on the P or H, it shows a mysterious dropdown with no indication of what it is. It'd be better if this dropdown automatically opened and started by highlighting the current value. That would make easier to see what it currently is, easier to change, and easier to see what the options are in the first place :-).

I propose adding a "renumber" option that renumbers steps. Hypotheses would be h1, h2, etc., while other steps would be 1, 2, 3, etc. (except for the last one).

When I do a "search" I can enter a pattern (great!). In addition, when I use patterns like 4 = or T. <-> I get very sensible results.

However, when I do some pattern searches I don't get the results I expect. Examples of surprises are ph <-> and class. In the first case, I get results that don't include the phrase ph <->. In the second, I seem to get everything that has a class type result in it... not everything with the constant term "class".

I think it'd be great to explain the pattern language where it's available. E.g., as a tooltip, or maybe a circled "i" for information that displays a longer explanation).

Also, it might be better if the pattern language metasymbols (like class) were unlikely to be math symbols in use. One way is to use "&" as a prefix, e.g., &class.

Also, it might be nice to support regular expressions as an option (add a checkbox "use regex"). Regexes are a widely-used pattern language that many people already know. Regular expressions don't know anything about the types of data (while this pattern search system does appear to), so perhaps they shouldn't be the default, but it'd be nice to have the option to use regexes for search. Since I don't fully understand the pattern language, I don't know what (or if) I'm missing :-).

When there's a generated proof, just before the goal statement's id include "$(" then the description text then "$)".

Metamath databases generally always have a description of each proven statement, it's odd to not include the description here in the generated proof. Currently a user has to copy-paste and recreate the descriptive comment, for no obvious reason.

The mmj2 tool enables someone to edit a single work variable into an expression, then press "unify" and automatically do a replacement of the work variables. So anyone who has used mmj2 will expect the same thing to work in metamath-lamp, even though it doesn't. Metamath-lamp does support replacement, but not in the same way.

It'd be very helpful if "unify" noted that work variables had been substituted with a specific expression, and then automatically apply applied that replacement everywhere if it had already occurred.

Sometimes you want to create a sequence of proofs: P1, P2, P3, where each depends on the previous one. It'd be nice to make that easy.

This presumes that inline text is implemented, #20 .

Modify the dialogue showing the compressed proof to add a new button, "transfer to context". This button on confirmation willcreate an inline text area in the context if one is not already there, and append the compressed proof to the inline text. It will then ask if you want to delete all statements (and do so on confirmation).

This creates a running accumulation of proofs in the inline text.

The worked example for 2+2=4 convinces me that the current default for "add statement" is wrong when no statement is selected. If no statement is selected and there's at least one statement, the new statement should be added just before the last statement. As long as you add the goal first (as recommended) this is the most likely place that the user wants a new statement added.

Currently I believe the default is to add the statement as the last statement. That is usually the right thing to do, but for a prover (like this) I think it's not the best default.

Making this change to the default will make the tool easier to use and easier to explain. It would, for example, eliminate a lot of steps in the 2+2=4 example.

I know you already plan to add some automation. I thought I'd add this issue as a way to track that. I think automation is the only major area where mmj2 has a significant advantage for typical proof creation.

You can find mmj2's automation heuristics here:
https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js
In short, when automation is enabled there are certain statements it always tries, and when it detects certain patterns it uses a simple algorithm to simplify it (e.g., for numbers). This automation is within its larger set of macros.

Mario can explain them in more detail.

Obviously it'd be awesome to have a full tactics language (including support for backtracking on failure). But simple automations could go a long way. Anyway, I know you're interested in that, so I thought I'd try to capture that idea here.

I'm not sure I understand what selecting statements in the bottom-up prover does.

That said, I have a thought. Perhaps this should be a 3-way option: Forbidden, Allowed, Required.

In particular, mmj2 allows specification of required statements at the first level, and this is often useful to force the use of specific statements - making searching much faster and making it more likely you'll find the proof you wanted. You might also add a button like "require use of previous statement" since in many cases you're adding a statement to extend on a previous one.

I haven't thought through all the ramifications, and there may be another/better way. But I thought it'd be better to record the thought before it disappeared from my head, and perhaps this idea will point the way to a good/better idea.

When in the search (magnifying glass) dialogue, ESC should escape it (Cancel), and the Enter key should "do the right thing" (select "Choose Selected" if that's allowed, otherwise do "Search").

When in the bottom-up proof dialogue, ESC should escape it. The Enter key should "do the right thing" (select "Apply" if that's allowed, otherwise select "Prove").

The same is true in other dialogue boxes - ESC should cancel out of it.

Add optional automatic "unify all" action right after the mm-lamp page loaded. This will add time for the initial loading. So experienced users may turn this off. But for new users this will allow them to see green checkmarks and visualizations without unifying first. This will be useful for small examples distributed via URL.

This also may be implemented via a parameter in the URL. So the author of the URL decides how the page should open. Probably this second option is better.