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 Le vendredi 9 août 2019 12:24:30 UTC+2, Noam Tene a écrit : > > 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. > > -- 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/089f3d33-7ddf-4824-be15-f8d1114f4d1c%40googlegroups.com.
