Hi Andrew, On Fri, Feb 4, 2022 at 11:35 PM Andrew Lubrino <[email protected]> wrote:
> 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 highly recommend the lean zulip chat https://leanprover.zulipchat.com/ for getting help with introductory issues. 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. > This is true, although for your own learning you can keep away from the heavy tactics. Theorem Proving in Lean is a book that starts right down at the basics, which might help in this regard. That said it's certainly true that metamath is considerably simpler in design than lean, even if you only consider the kernel and not all the surrounding tactic stuff. 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? > What you are describing is the difference between Natural Deduction (or Gentzen-style deduction) and Hilbert-style axiomatizations. Metamath is a Hilbert style system, which means that there is no local context of assumptions that can be discharged during the proof. However, it is possible to simulate natural deduction proofs with very little syntactic overhead, and I highly recommend using this style for practical formalization in metamath. In the case of proving an implication, this means an application of theorem "ex" (http://us.metamath.org/mpeuni/ex.html), where we are proving |- Gamma -> (x -> y) and we reduce this to showing |- (Gamma /\ x) -> y. In this proof style, we maintain an implication at the top level more or less at all times, where the things on the left of the implication are the simulated local context. So Gamma here would be a conjunction of everything else going on at this point in the proof, and in the subgoal we have added x to that conjunction, i.e. we've assumed x. See http://us.metamath.org/mpeuni/mmnatded.html for further reading, and http://us.metamath.org/mpeuni/natded.html for a cheat sheet showing how to translate individual ND inferences to metamath theorems. 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? I have a bit of familiarity with Mizar but the syntax really shows its age, and there isn't a very strong metatheory behind it - many things feel very ad-hoc, and there is no small trusted kernel. The fact that it is not open-source is also a big turnoff for me, but perhaps that's not an issue for you. (I believe it's not too hard to get in the Association of Mizar Users, and then you can have a peek at the code.) 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? > There are a few ways, depending on your disposition. You can read a regular math or logic textbook, and try to find analogues of the theorems in metamath or prove them yourself. (This works especially well for books that are referenced a lot in theorems.) You can also pick a medium sized theorem and try to prove it by working backwards to other theorems every time you find a missing prerequisite. You can also try to shorten existing proofs or come up with alternative ways to a proof, which was very productive for me to get acclimated to the library. Reproving theorems that already exist isn't such a huge draw for me at least if I'm not making the proof better in some way by the process. There are cofinitely many theorems left to prove, many of them quite elementary, so striking out into a new area is probably more comfortable for a newcomer compared to retrodding old paths or adding to a complex theory. I'm not sure that metamath (or other formal system) is a good choice for learning new mathematics on its own, but it makes a great supplement to existing mechanisms for learning, and I learned a huge amount of the mathematics I know from a combination of wikipedia, metamath, and other "nontraditional" internet sources. (Which is part of why I don't write as many references as I should...) Mario Carneiro -- 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/CAFXXJSs_3m9h_3cbUKad%3DqAPbruZUAqBRAw8Orgh%3DGua6W9i9A%40mail.gmail.com.
