Wow this is all good advice. Thank you both for the responses. So do you both think I should go back and continue working with Lean and try to figure out my problems?
Also, when I say abstract math, I think I’m really just looking to learn the topics in an introductory discrete math course. I want to learn about set theory, which includes Cartesian products, families of sets, functions, and relations. I ultimately would like a system that I could use to verify proof problems from a graph theory or algorithms text. I’m pretty sure what I’m looking to learn might actually be formal logic. Does this change your opinion about what I should be using? I have a lot to think about, but it does seem like Lean might still be my best bet. I’ll have another go at it, but I think I’ll still experiment with mm since it’s so dead simple anyway. Thanks! On Sat, Feb 5, 2022 at 6:26 AM vvs <[email protected]> wrote: > 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 a topic in the > Google Groups "Metamath" group. > To unsubscribe from this topic, visit > https://groups.google.com/d/topic/metamath/lO3PPEkLet0/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/8d6c57ae-198e-4cff-98b8-9b12d51e746dn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/8d6c57ae-198e-4cff-98b8-9b12d51e746dn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAOcJWNHe7rsHLf2t-qh1LyUghxCx3G9%3DMDcndFyFT-kbpQZcdA%40mail.gmail.com.
