Hi Andrew, 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.
I would argue, that using tactics is an advantage for a beginner. This is exactly because they should hide many boring technical details which are exposed by a term style proofs. Metamath is good for verifying and studying existing proofs but has little support for their synthesis. > I'm sorry if this is a stupid question, but if I learn math with mm, will > I be learning the "right" math? As Kevin Buzzard frequently said, you should not attempt to learn math and formal logic at the same time and he is an expert. It's a double burden and you *don't need* one to learn the other. I'd recommend to learn them sequentially and not in parallel. > > 1. 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? > > There are some people out there who reproved many MM theorems from scratch, but I don't know their level of proficiency in mathematics. Mario Carneiro is one of the best professionals in the field so don't try to compare with him :) But take any advice with a grain of salt because all people are different. -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8d6c57ae-198e-4cff-98b8-9b12d51e746dn%40googlegroups.com.
