> On Feb 11, 2023, at 5:00 AM, Igor Ieskov <[email protected]> wrote: > > Thanks David!
You're very welcome! This version really has come a long way: https://igorocky.github.io/mm-proof-assistant/demo/v5/index.html One broad suggestion: Could you give it a short & less generic name, since there are other Metamath proof assistants? Naming is hard, but a short unique name will make it easier to discuss & find. And I think this is *very* worthy of discussion & being found. You might want to include, on the screen or an "about" option, a link to the GitHub repo for the code (so people can review/contribute). I understand that is currently: https://github.com/expln/metamath-proof-assistant (MIT license). > >>> What are the "key" things you think it's missing, especially in > >>> comparison to mmj2? > > 1) I think one of the "key" missing things is ability to help a user to > understand why a statement doesn't unify. As also Thierry noted earlier, > currently the app shows only this message "Justification cannot be determined > automatically". Or another message is possible too "Justification for this > statement is incorrect". But the app doesn't explain what is the reason. > That's my next goal. I don't see any trivial or simple solution, so it may > take some time to implement. Whoa, that's a very high bar. I suggest working on other things first & getting back to that later (if ever). In particular, if you add tactics & some automation, the reason for that answer will change, so I suggest working on some predefined tactics/heuristics first. If your intent is to just determine why "this statement doesn't unify with this other specific statement", you could try to find the longest match & identify where it finally fails. That seems doable. You could even walk across the database & report the longest incomplete match, but I don't know if it'd be helpful; it'd probably report some very general but unrelated theorems. But I think trying to answer "why can't I automate this in general" is best delayed for a long time. I can be wrong, of course :-). > 2) Another, although maybe not a "key" thing, is to have predefined "tactics" > to prove some common cases, for example, prove by induction or prove by case > analysis. This not necessarily has to result in complete ready proofs, but it > may create another new statements which help a user to move in the desired > direction (similar to what I saw in Coq proof assistant). > > 3) As you mentioned mmj2 uses some useful heuristics. I also would like to > add heuristics to improve automatic proof search. You could easily combine 2 & 3. Just create a first tactic called "auto" or similar that tries to apply a few simple rules to automatically prove a few simple/common cases. I would devise them so that eventually tactics could be called internally (e.g., by other tactics & maybe even a scripting language). Then make it so a user can select a tactic to a selected set of statements, and you're off. mmj2 has a few simple heuristics that it applies automatically its default configuration. You could make them either fully automatic or the basis for an "auto" tactic. Code here (I think Mario wrote more or all of this): > https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js Don't feel you have to use it exactly, and it might be better split into different tactics (mmj2 doesn't really support multiple different tactics, a big weakness of it). Even a few small automations could make a big improvement in usability. > 4) Finally, not key at all, but what should improve user experience and may > be achieved relatively easy (implementation still may require a lot of time > but at least everything is clear for me in terms of how to implement): User experience improvements can make a big difference. I think that's more key than you realize, and I bet a few easy ones would make all the difference. > a) exit edit mode by pressing ESC key Yes! Existing with the ESC key would be a big help. > b) highlighting syntax subtrees by clicking them To simplify replacing them, I guess? > c) graphical visualization of justifications Graphical visualization of justifications is probably not very helpful, they tend to be a mess once they become non-trivial. I would instead prefer an optional simple column, to the left of the statement proved, showing JUSTIFICATION_NAME LIST_OF_REFERRED_STATEMENTS (similar to how mmj2 works now). I'd also make the default statement names shorter (so that justification text takes less space), e.g., shorten "stmt" to "s" or some such. In the future, as a bonus, it'd be nice to be able to rename step names - they don't matter for the final proof, but it might make proving things easier. > d) proof explorer for the loaded *.mm file A nice-to-have, but I think you can delay that. The metamath website already provides a proof explorer that people can use. You could provide a link that opens a new tab to us.metamath.org and get a lot of the way there. > e) sharing proofs via URLs (as you suggested and I find this very useful for > collaboration). I want to implement this after some time, because when I > implement it, I will have to support backward compatibility between different > versions, so I want to wait when internal representation of the editor state > becomes stable (no frequent changes in the code). Cool, glad you liked the idea. The rationale for delay makes sense, though I can't wait to use it :-). Once you implement 4(e), undo/redo becomes trivial (you can let the browser do it!). I suspect there's no need to compress it, and you'll get decent results from encodeURIComponent(JSON.stringify(your_representation_here)). Of course, there's the question of what your_representation_here is :-). Just don't stick the whole MM database in there :-). > Currently my plan is to work on the 1st and 4th items. As I said, I'd delay #1 (that is likely to be *hard* unless you really back off on your plans). I'd love to see small increments on #4, and a little automation (#2/3). Regarding user improvements, most people will want to load the current set.mm & iset.mm, so making that easier would be helpful. If there was an easy way to download it straight from the web, that might make getting started easier. I could easily configure us.metamath.org's CORS settings so the script could always download .mm files from us.metamath.org no matter where it started from. You might want to walk through the mmj2 tutorial to see what ideas are worth stealing. I recorded it on Youtube here: https://www.youtube.com/watch?v=87mnU1ckbI0 The text is here: https://github.com/digama0/mmj2/tree/master/mmj2jar/PATutorial Once you're further along, I'd be happy to work with you to create a tutorial if you'd like. I'd probably want to build on the same examples from the mmj2 tutorial. It's your project, so take my comments with a bucket of salt. I really do think this is neat though! --- 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/C2593B77-C1F2-45F5-8523-E347EEF5C569%40dwheeler.com.
