Hello, I'm just getting started with Metamath. I have mm and mmj2 installed on my computer and I've been able to prove the first few theorems in set.mm independently, so I know my setup works. I have a few questions about mm and its suitability for my purposes:
1. I don't have a background in abstract math, but I'm looking to learn with an interactive theorem prover as a feedback system. I started with Lean about 1 month ago, but I started to try proving properties of families of sets and cartesian products and I was bogged down by tons of technical stuff and I just gave up after a few days because I couldn't figure out the right syntax. I think the problem with Lean for a beginner is that it makes heavy use of tactics, which obscures what's actually happening in the proof. I'm interested in mm because it's very simple and tactics aren't part of the system. It would be hard to get bogged down with lots of technical detail. But the structure of a proof in mm is very different than anything I've seen. For example, x implies y is normally proven by assume x, show y, but mm doesn't seem to allow that. I'm sorry if this is a stupid question, but if I learn math with mm, will I be learning the "right" math? 2. I was thinking of using Mizar for my purposes. Mizar is also much simpler than Lean or Coq in that it doesn't make heavy use of tactics. The proof style of Mizar also seems much more conventional (and better looking) than mm. My only problem here is that there doesn't seem to be a really active community around Mizar and it is still possible to get bogged down by technical stuff (the typing system is confusing for me with Mizar). For learning abstract math, what is the group's opinion on choosing Mizar vs mm? 3. If I do use mm, is there a good way to go about systematically learning the math content? This evening, I started with the first theorem in set.mm and proved about the first 5 or 6 theorems. Should I just try to sequentially prove every theorem in set.mm? Or is this way too much? What's a better strategy? Thanks very much for reading this. Andrew -- 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/bad17dd1-8042-4bab-9c98-d015cde2d1a2n%40googlegroups.com.
