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 <https://jiggerwit.wordpress.com/2018/04/14/the-architecture-of-proof-assistants/>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 <https://www.reddit.com/r/ProgrammerHumor/comments/cnyxtm/overprotective_me/> 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 <https://groups.google.com/forum/#!searchin/metamath/exercises%7Csort:date/metamath/ADFVZxmWUtg/IMOgWeItBwAJ> 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 <http://us.metamath.org/mpegif/lawcos.html> 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 <http://us.metamath.org/mpegif/iocunico.html>, 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 <http://us.metamath.org/mpegif/conventions.html>. 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 -- 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/6df90e60-f791-47cd-84fb-4980029b6221%40googlegroups.com.
