Metamath vs Mizar for someone new to abstract math

[Andrew Lubrino]

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 

[Mario Carneiro]

Hi Andrew,

On Fri, Feb 4, 2022 at 11:35 PM Andrew Lubrino <andrew...@gmail.com> 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

[vvs]

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.

[Andrew Lubrino]

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!

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8d6c57ae-198e-4cff-98b8-9b12d51e746dn%40googlegroups.com.

[Jim Kingdon]

You are probably ready to try out one or more prover systems (or keep trying out in the case of lean) rather than collect more opinions, but I'm pretty sure either Lean or methamath set.mm would be suitable in terms of being able to do things with functions, relations, integers, etc (and not have to start from scratch on everything). Hope it isn't intimidating to post the tables of contents of their math libraries, but it is https://leanprover-community.github.io/mathlib-overview.html for lean and http://us.metamath.org/mpeuni/mmtheorems.html for set.mm - I post this just to show that either one of these systems formalizes a bunch of different areas of mathematics.

Personally, I dabbled in trying to learn the type theory based systems (coq and isabelle in my case, I suppose it would be lean today) and I kept coming back to metamath (or now-defunct metamath-like systems). But this could be as much happenstance (in terms of which ones I encountered first or first had a reason to get proficient in) as anything which would have made it difficult for me to learn the others.

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAOcJWNHe7rsHLf2t-qh1LyUghxCx3G9%3DMDcndFyFT-kbpQZcdA%40mail.gmail.com.

[vvs]

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?

In that case, your choice of using formal systems to learn about logic looks just right to me. In addition to what Mario suggested above, did you look at Lean and Coq learning resources? There are a lot of online books about logic and software foundations. Also, I wouldn't discount some logic puzzles, like natural number game if you didn't try it out yet.

[vvs]

Personally, I dabbled in trying to learn the type theory based systems (coq and isabelle in my case, I suppose it would be lean today) and I kept coming back to metamath (or now-defunct metamath-like systems). But this could be as much happenstance (in terms of which ones I encountered first or first had a reason to get proficient in) as anything which would have made it difficult for me to learn the others.

I wonder if you have CS or math background. In my experience, the language is a defining factor for most programmers, especially familiar with functional programming. And they should feel right at home using dependently typed programming languages vs. set theory. Although, there is Lisp, of course, but it has abstract syntax at least. For me, the ad-hoc syntax which uses Metamath is the biggest obstacle and tactics come after that. The whole experience reminds me programming in assembler language which is nice in simple cases, but becomes annoying when it is too complex. The irony is that while Metamath is trying to be faithful to traditional mathematical notation, mathematicians are adopting programming languages, like Lean (or even APL like Iverson) at the same time.

My first motivation which turned my attention to Metamath was a desire to look at all the gory details of a proof. But soon I found out that I don't really need them all. What I needed instead was a confidence in a proof verifier and the level of details that is "just enough" to understand full argument. Too much technical details actually distracts me from the ideas and I can't see the forest for the trees. And while I can fold the proofs on the web it is still boring to use mmj2 for that. But that's just me, of course. All people are different.