Resources for newbies

[ginx]

Hi! and sorry if this is not the right place for this type of post. I recently found out about Metamath and I couldn't help but be impressed by just the sheer concept of it all. I want to get deeper into it, however, as a CS student with very little knowledge on mathematical logic or set theory, I don't really know what the best way for me to start is.

If you have any recommendations of books, areas of interests or online resources someone with my level (essentially zero, though I’m well acquainted with more formal proofs because of math Olympiads) could read to get started, I would much appreciate it.

By around June or July of 2021 I need to deliver a dissertation in order to graduate and I would love it if it could be about some Metamath project, like formalizing some theorem (doesn’t need to be a very complicated one) that has yet to be formalized. I read about the 100 theorems but I’m unsure if I could get one of those within the allotted time. So feel free to recommend me some unformalized theorems as well, I would much appreciate it.

Thanks for reading, and I greatly appreciate any help,

ginx.

[Norman Megill]

Welcome!

I wouldn't dismiss the 100 theorem list out of hand.  Many of them were done by non-mathematicians with a CS bent.  It looks like you have 8 or 9 months to work on this, but even if in the end you discover you bit off more than you can chew, the background material that you do develop can help someone else complete it in the future.

The people here are very helpful and would probably be willing to guide you through the process in terms of outlining what background material needs to be developed (which is important to get right so you won't waste a lot of time going down a wrong path), help you with proofs that you get stuck on, etc.  Don't hesitate to ask even the most basic questions like how to get started with Metamath.

Many of the proofs that Metamath is missing have been done with other provers.  David Wheeler built a list of these, along with how many other provers have proved the theorem.  That can provide a rough idea of the difficulty - the more provers that have done a proof, the more likely it is feasible in Metamath.

https://groups.google.com/g/metamath/c/QPOfJEnRqmU/m/zTt4GGiZDgAJ

This list from 2016 is out of date, though.  David provided a python program there to regenerate it; perhaps you can re-run it and post the updated list here.

In principle a proof from another prover can even provide a guide for the Metamath version, although I don't know if anyone has actually exploited this.  Some familiarity with the other proof language would be needed to understand its proof, although that might not be bad thing since it would broaden your background.

Norm

[Stanislas Polu]

Tangentially, OpenAI would be more than happy to provide you with access to our proof assistant. For what it’s worth, internally, it has helped us a lot getting up to speed with Metamath and more particularly its library.

More details are available here if interested: 

https://groups.google.com/g/metamath/c/D09W2QVR-_I/m/g_rsqGj0AAAJ

Best,

-stan

--


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/e0364c41-9804-43fe-8117-b796a73a242an%40googlegroups.com.

[Norman Megill]

On Monday, September 7, 2020 at 12:59:59 PM UTC-4 Norman Megill wrote:

...

 

Many of the proofs that Metamath is missing have been done with other provers.  David Wheeler built a list of these, along with how many other provers have proved the theorem.  That can provide a rough idea of the difficulty - the more provers that have done a proof, the more likely it is feasible in Metamath.

https://groups.google.com/g/metamath/c/QPOfJEnRqmU/m/zTt4GGiZDgAJ

This list from 2016 is out of date, though.  David provided a python program there to regenerate it; perhaps you can re-run it and post the updated list here.

It looks like Google stripped the leading spaces from the python program.  @David, did you save this program, and if so could you run it for us to get an updated list?  Thanks.

Norm

[David A. Wheeler]

It's a holiday in the US, and I currently have the very important job of grilling burgers. But I will try to get to that later today. :-)
--- David A.Wheeler

[David A. Wheeler]

On Mon, 7 Sep 2020 14:23:41 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> > Many of the proofs that Metamath is missing have been done with other
> > provers. David Wheeler built a list of these, along with how many other
> > provers have proved the theorem. That can provide a rough idea of the
> > difficulty - the more provers that have done a proof, the more likely it is
> > feasible in Metamath.
> >
> > https://groups.google.com/g/metamath/c/QPOfJEnRqmU/m/zTt4GGiZDgAJ
> >
> > This list from 2016 is out of date, though. David provided a python
> > program there to regenerate it; perhaps you can re-run it and post the
> > updated list here.
> >
>
> It looks like Google stripped the leading spaces from the python program.
> @David, did you save this program, and if so could you run it for us to get
> an updated list? Thanks.

I didn't save the code, but it was easy to reconstruct its indentation.
I also tweaked it to make its results prettier.

Here are the results:

4 6. G&ouml;del's Incompleteness Theorem
3 84. Morley's Theorem
3 40. Minkowski's Fundamental Theorem
3 36. Brouwer Fixed Point Theorem
3 28. Pascal's Hexagon Theorem
3 13. Polyhedron Formula
3 100. Descartes Rule of Signs
2 99. Buffon Needle Problem
2 8. The Impossibility of Trisecting the Angle and Doubling the Cube
2 53. Pi is Transcendental
2 29. Feuerbach's Theorem
2 12. The Independence of the Parallel Postulate
1 92. Pick's Theorem
1 56. The Hermite-Lindemann Transcendence Theorem
1 50. The Number of Platonic Solids
1 47. The Central Limit Theorem
1 41. Puiseux's Theorem
1 32. <u>The Four Color Problem</u>
1 21. <u>Green's Theorem</u>
0 82. Dissection of Cubes (J.E. Littlewood's "elegant" proof)
0 62. <i>Fair Games Theorem</i>
0 59. <i>The Laws of Large Numbers</i>
0 43. <i><u>The Isoperimetric Theorem</u></i>
0 33. <i><u>Fermat's Last Theorem</u></i>
0 24. <u>The Undecidability of the Continuum Hypothesis</u>
0 16. <i>Insolvability of General Higher Degree Equations</i>

This is only an *estimate* of current achievability, of course.
I'd love to hear comments of where people think the theorem is
more or less achievable given the start of set.mm.

I'll create a pull request to add this script to the scripts subdirectory.

Aside: I created an indentation-sensitive syntax for Lisp, called Sweet Expressions,
which supports "!" as an indent character. Among other things that
prevents this "gobbling" of leading whitespace.

--- David A. Wheeler

[Thierry Arnoux]

Hi ginx!

Welcome to the community!
It’s perfectly fine to use this group for an introduction and as a call for help!
It sounds like Metamath is a great idea for a graduation project.

I would be a bit careful with David’s list, some theorems might be high on the list because they are very relevant, not because they are very easily formalizable, but it’s still a good reference.

Even though the basic principles are very simple, it takes skill and mileage to find which elementary theorem to apply to reach your goal and build a MM proof. Tools like OpenAI assistant and MMJ will help greatly for that.

Which area of the mathematics are you more interested in?

I would recommend a domain where you feel comfortable, so that not both the Maths and the Metamath are new.

So besides the 100 theorems, you might also look at Math theorems you have learnt in your CS curriculum and which might not have been formalized yet.

Again, welcome, and I wish you a lot of fun!
BR,
_
Thierry


> Le 8 sept. 2020 à 09:18, David A. Wheeler <dwhe...@dwheeler.com> a écrit :

> --
> 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/E1kFSHG-0006Uy-LF%40rmmprod06.runbox.

[David A. Wheeler]

On Tue, 8 Sep 2020 10:31:37 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> I would be a bit careful with David’s list, some theorems might be high on the list because they are very relevant, not because they are very easily formalizable, but it’s still a good reference.
>
> Even though the basic principles are very simple, it takes skill and mileage to find which elementary theorem to apply to reach your goal and build a MM proof. Tools like OpenAI assistant and MMJ will help greatly for that.

I agree. Start with something absurdly simple, so you're not trying to learn too many things simultaneously.

I posted some Metamath-related video tutorials on Youtube. You may find them helpful.

--- David A. Wheeler

[drjonp...@gmail.com]

Hi Ginx :)

One thought: maybe as a CS student you might find it easier to work on the tools side of the project rather than the mathematical side? For example you could write a parser or verifier as your project? That's a CS problem rather than so mathematical.

Also I imagine if you have time to work on code you could have a look at metamath.exe or mmj2 and see if there is anything you could contribute there?

One tool I was thinking of writing, but I have no energy, is one where you can post an incorrect mm statement and the tool can try to tell you what is wrong with it. So for example it can count opening and closing brackets for you, and also check if all tokens are valid mm tokens etc. This is something no one has done before but could be a really helpful thing to have I think and might not be so difficult.

In terms of learning mm the approach I took was to read the book, watch David's videos and then do Filip's nice problems. I'd also recommend the OpenAI tool, and has it's own practice problems, it's really fun and makes me feel really cool just to have access to it ha ha. If you do go that way here are the problems I have done with it to help in case you get stuck, though I am not so expert.

Jon

[Jim Kingdon]

Ooh, that's an interesting idea (I mean, there are plenty of mathematical possibilities, if that interests you, including theoretical computer science related math, but there is no shortage of tools too). In addition to what is mentioned here (I love the proposed "why is this a syntax error?" tool), giving the definition checker some love would be a possibility, including writing a testsuite (of negative and positive cases), reimplementing it outside mmj2, or anything else.

[ginx]

Hi! and thanks for all the replies, I definitely wasn't expecting so many! I will address all of your kind replies:

Norm:

Thanks for the reply, I’m definitely going to hang out around here more often. The 100 theorems is my ideal option, I was scheming the list provided and some theorems caught my eye, like the four colors one, however, that one has only bene proven by Coq, so it might out of hands for me (at least for the purpose of the dissertation). The Insolvability of General Higher Degree Equations also caught my eye, but that one is even worse since it appears to have no formalized proof by prover yet. Descartes Rule of Signs is one that I’m already familiarized with and 3 provers already have it so this one could be a good option.

Other than that, I’ve got a couple of theorems in mind that do not belong to the 100 theorems. Erdős–Szekeres theorem, Chinese remainder theorem, Kummer's theorem, Lucas's theorem and others. Or maybe just check the validity and/or worst time/space complexity of some CS algorithms, such as: Kosaraju's algorithm, KMP algorithm, Sieve of Eratosthenes (regular one and linear time one), and others. Maybe even for data structures as well. Main problem is, I’m not sure which of these have already been solved in Metamath or are currently being solved. Is there some sort of index to check for this?

 

Stan:

Thanks for the reply, that tool seems pretty useful. I’d be interested in using it once I get a little bit more familiarized with the plain Metamath. I’ll send you an email :)

 

David A. Wheeler:

Thanks for the replies, hope the burger grilling went well for you.

I’m definitely going to watch all of your Metamath videos. Is there some sort of specific background expected in order to watch them?

 

Thierry:

Thanks for the reply and the advice. I was unsure if this was a forum to discuss exclusively for already advanced users or else, but now I definitely will ask more questions in the future.

I’m mostly interested in combinatorics, number theory and just regular CS algorithms. Previously I listed a couple theorems on those areas that I already feel comfortable with.

Thanks for the good wishes and good luck!

 

Jon:

Hi! Though the idea of working more on tools sounds interesting, I’m really more interested in working with proofs, since it’s a topic that I really like. I’m certainly open to the idea of contributing in the future.

Thanks for the resources, I’m going to check the problems and the videos for sure. I quickly skimmed through the book and it does touch on some set theory, should I perhaps read more about it before jumping into this book?

Thanks :)

 

Kin (sorry, I can’t really see your full address):

Thanks for your suggestion, it does sound like something that can be very useful so I’ll keep it in mind for the future (if someone else doesn’t do it first).

[Norman Megill]

On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote:

Norm:

Thanks for the reply, I’m definitely going to hang out around here more often. The 100 theorems is my ideal option, I was scheming the list provided and some theorems caught my eye, like the four colors one, however, that one has only bene proven by Coq, so it might out of hands for me (at least for the purpose of the dissertation). The Insolvability of General Higher Degree Equations also caught my eye, but that one is even worse since it appears to have no formalized proof by prover yet. Descartes Rule of Signs is one that I’m already familiarized with and 3 provers already have it so this one could be a good option.

Other than that, I’ve got a couple of theorems in mind that do not belong to the 100 theorems. Erdős–Szekeres theorem, Chinese remainder theorem, Kummer's theorem, Lucas's theorem and others. Or maybe just check the validity and/or worst time/space complexity of some CS algorithms, such as: Kosaraju's algorithm, KMP algorithm, Sieve of Eratosthenes (regular one and linear time one), and others. Maybe even for data structures as well. Main problem is, I’m not sure which of these have already been solved in Metamath or are currently being solved. Is there some sort of index to check for this?

There is an outline of the set.mm content here:
http://us.metamath.org/mpeuni/mmtheorems.html
although it doesn't always show specific theorems on the Table of Contents page but just the general area covered by a section.

The Erdos–Szekeres theorem and the Chinese remainder theorem are here:
http://us.metamath.org/mpeuni/erdsze.html
http://us.metamath.org/mpeuni/crt.html

You can click on "Nearby theorems" on the above pages to see related material.  The small colored number after a theorem label will let you determine where it falls in the  mmtheorems.html table of contents.

(It looks like erdsze is still in Mario's "mathbox" [which is a work space assigned to individuals for developing proofs - you will get one].  Since it is one of the mm100 theorems, at some point it probably should be moved to an appropriate place in the main body of set.mm.)

BTW I found the above theorems by searching set.mm in the metamath program:

./metamath
MM> read set.mm
MM> search * szek /comment
MM> search * chinese /comment

Other tools like mmj2 also have search functionality, and worst-case there's grep :)

Since Mario did the above 2 proofs, perhaps he has comments on some others on your list, such as to what extent we have the necessary background material developed.

Norm
 

[Mario Carneiro]

On Wed, Sep 9, 2020 at 5:58 PM Norman Megill <n...@alum.mit.edu> wrote:

On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote:

Norm:

Thanks for the reply, I’m definitely going to hang out around here more often. The 100 theorems is my ideal option, I was scheming the list provided and some theorems caught my eye, like the four colors one, however, that one has only bene proven by Coq, so it might out of hands for me (at least for the purpose of the dissertation). The Insolvability of General Higher Degree Equations also caught my eye, but that one is even worse since it appears to have no formalized proof by prover yet. Descartes Rule of Signs is one that I’m already familiarized with and 3 provers already have it so this one could be a good option.

Other than that, I’ve got a couple of theorems in mind that do not belong to the 100 theorems. Erdős–Szekeres theorem, Chinese remainder theorem, Kummer's theorem, Lucas's theorem and others. Or maybe just check the validity and/or worst time/space complexity of some CS algorithms, such as: Kosaraju's algorithm, KMP algorithm, Sieve of Eratosthenes (regular one and linear time one), and others. Maybe even for data structures as well. Main problem is, I’m not sure which of these have already been solved in Metamath or are currently being solved. Is there some sort of index to check for this?

There is an outline of the set.mm content here:
http://us.metamath.org/mpeuni/mmtheorems.html
although it doesn't always show specific theorems on the Table of Contents page but just the general area covered by a section.

The Erdos–Szekeres theorem and the Chinese remainder theorem are here:
http://us.metamath.org/mpeuni/erdsze.html
http://us.metamath.org/mpeuni/crt.html

You can click on "Nearby theorems" on the above pages to see related material.  The small colored number after a theorem label will let you determine where it falls in the  mmtheorems.html table of contents.

(It looks like erdsze is still in Mario's "mathbox" [which is a work space assigned to individuals for developing proofs - you will get one].  Since it is one of the mm100 theorems, at some point it probably should be moved to an appropriate place in the main body of set.mm.)

I was still running on the assumption that metamath 100 theorems in a mathbox are fine, but we can move this theorem into main if you like.

Since Mario did the above 2 proofs, perhaps he has comments on some others on your list, such as to what extent we have the necessary background material developed.

Sure:

On Wed, Sep 9, 2020 at 6:06 AM ginx <favax...@lywenw.com> wrote:

I was scheming the list provided and some theorems caught my eye, like the four colors one, however, that one has only bene proven by Coq, so it might out of hands for me (at least for the purpose of the dissertation).

Don't try, it took Gonthier six years with a team of people to do.

The Insolvability of General Higher Degree Equations also caught my eye, but that one is even worse since it appears to have no formalized proof by prover yet.

I expect this one to appear in lean soon, or at least there are motions in that general direction. The hard part for doing this in metamath is developing the necessary Galois theory; there is some work on field extensions in my mathbox but not nearly enough. That's not to say you shouldn't try it, particularly if you have some experience with the mathematical prerequisites already, but there will be a decent amount of library building involved.

Descartes Rule of Signs is one that I’m already familiarized with and 3 provers already have it so this one could be a good option.

This one does not look so hard, and we have some basics on polynomials and divisibility already, so this looks like a good choice.

Other than that, I’ve got a couple of theorems in mind that do not belong to the 100 theorems. Erdős–Szekeres theorem,

Already done as Norm noted, but there are lots of other combinatorics theorems that haven't been done if you are interested in this area.

Chinese remainder theorem,

There are many *many* variations of CRT that vary widely in generality. We have the most basic form of it, but the version using ideals hasn't been done AFAIK.

Kummer's theorem,

I hadn't heard of this one, but it sounds quite close to some of the analysis that is done in Bertrand's postulate, specifically http://us.metamath.org/mpeuni/pcbc.html, which also involves counting the multiplicity of primes in (central) binomial coefficients. I don't know how you would define "number of carries" but it might be a short hop from pcbc.

Lucas's theorem

I don't think we have this one, but it looks like a simple proof given the available background.

Or maybe just check the validity and/or worst time/space complexity of some CS algorithms,

There is a lot more library building involved in this than I think you anticipate. You have to define a model of computation, prove that it's not degenerate (which is to say, prove that lots of interesting constructions are computable), and a way to count steps. While I would be very excited to see some of this (I built a similar development of computability theory in lean), it is a pretty big project.

such as: Kosaraju's algorithm,

There is some graph theory needed for this, but not too much. You might be able to fake the computational substrate a bit with a very high level computational model, if you want to skip the library building part; it is possible to express "number of steps" using a simple abstract dynamical system instead of something like a turing machine that would introduce a lot of incidental complexity here. I would say Metamath is not the best choice for this formalization, at least not at this stage.

KMP algorithm,

Same problem. The algorithm itself is easy, but the library building is huge. You want a framework for doing these kinds of proofs, and metamath doesn't have it. (I am currently working on a framework for doing program correctness proofs in metamath zero, but it will be a while before it gets hooked back up to metamath.)

Sieve of Eratosthenes (regular one and linear time one), and others.

I don't think it's linear time BTW. Wikipedia says it's O(n log log n) with a random access machine, and if you use a turing machine it's probably at least O(n^2), and with a pointer machine (or a metamath proof) at least O(n log n).

Maybe even for data structures as well. Main problem is, I’m not sure which of these have already been solved in Metamath or are currently being solved. Is there some sort of index to check for this?

CS applications are not particularly well covered in metamath. Lean (and Coq and Isabelle although I don't work with those as much) are much further along in these areas because they are written by computer scientists. The whole "do everything by hand" approach really loses its appeal when the theorem statements are large and technical. Some automation customized to the framework is required.

Mario

 

[ginx]

Thanks for those resources Norm, it seems like a very throughout list. I haven’t installed mmj2 yet, so I didn’t know you could just search like that, pretty useful.

Also, I believe that erdsze is not really part of the 100 theorems, so maybe it should stay on the mathbox (?). I believe only Ramsey’s theorem belongs.

 

Also, thanks for the very detailed explanation Mario. After reading it, I think I basically boiled it down to just two possibilities: Descartes Rule of Signs, which as you stated should be doable, and the CS route. Though it might require a lot more library building, I think I incline more towards the second option. As Norm stated before, even if I can’t complete an entire proof, it can certainly be useful to work on the libraries to make it happen in the future, and I’m sure my teachers will understand  as well (is only bs level dissertation, not a masters one).

As to what specific algorithm, I’m really not sure right now. I guess after I manage to do even an extremely simple, equivalent of 2+2=4, one then I’ll see what I can get into. Kosaraju can be a good option in order to open up the graph theory possibilities in the future. Oh and about the Sieve, I was referring to a specific implementation that reduces the time complexity by increasing the space one: https://cp-algorithms.com/algebra/prime-sieve-linear.html.

Also, you also mentioned that you’re working on a framework for correctness proof, would you also include tools for counting number of steps and other elements or just the correctness? Around how much time do you think it will take you? Mostly out of curiosity since I plan on working on the tools myself regardless of the framework.

Lastly, I would definitely check out the other tools, at the very least to expand my views on the subject. Which one would you recommend for a beginner? Isabelle is the only one that I checked before Metamath.

Thanks,

ginx.

[Mario Carneiro]

On Thu, Sep 10, 2020 at 5:36 AM ginx <favax...@lywenw.com> wrote:

Also, thanks for the very detailed explanation Mario. After reading it, I think I basically boiled it down to just two possibilities: Descartes Rule of Signs, which as you stated should be doable, and the CS route. Though it might require a lot more library building, I think I incline more towards the second option. As Norm stated before, even if I can’t complete an entire proof, it can certainly be useful to work on the libraries to make it happen in the future, and I’m sure my teachers will understand  as well (is only bs level dissertation, not a masters one).

As to what specific algorithm, I’m really not sure right now. I guess after I manage to do even an extremely simple, equivalent of 2+2=4, one then I’ll see what I can get into.

That's a good outlook. Even if you never make it past 2+2=4 the library building itself could be a paper or two. If you want a simple example, I would suggest Euclid's GCD algorithm, as metamath already has a sort of pure version of that without the runtime bounds or computational model, so all the necessary pure math stuff is already done and all you need to add is the CS stuff.

Kosaraju can be a good option in order to open up the graph theory possibilities in the future. Oh and about the Sieve, I was referring to a specific implementation that reduces the time complexity by increasing the space one: https://cp-algorithms.com/algebra/prime-sieve-linear.html.

Also, you also mentioned that you’re working on a framework for correctness proof, would you also include tools for counting number of steps and other elements or just the correctness? Around how much time do you think it will take you? Mostly out of curiosity since I plan on working on the tools myself regardless of the framework.

Oh, my framework is a pretty massive project. It probably won't be useful for your purposes before you are done with your dissertation. Plus it's not directly applicable to proofs in metamath (it's a different logical system, very similar to metamath but requiring a translation layer). You can read about it here -> https://arxiv.org/abs/1910.10703 , or on the various posts on this forum about Metamath Zero or Metamath C.

The framework is focused on correctness proofs of real software. As such it is a little too concrete for nice proofs of theoretical CS algorithms. It could also be extended to support reasoning about runtime but that's not on the agenda for now.

Lastly, I would definitely check out the other tools, at the very least to expand my views on the subject. Which one would you recommend for a beginner? Isabelle is the only one that I checked before Metamath.

I'm pretty partial to Lean, since I am personally involved in the library maintenance there as well. In particular, there is a really great Zulip chat room (https://leanprover.zulipchat.com/) about Lean that is very friendly (to people of all skill levels) with plenty of smart people and mathematicians and me :) .

Mario

[ginx]

Oh I see, I will check out more of the Metamath Zero project, since it sounds very interesting.

I will check more about Lean though I think I will still do my project on Metamath. Also, good luck with zero!

Now that I have a more clear direction of where to go, I know better where to start, so thanks to everyone on the thread.

[tbrend...@gmail.com]

A tip I have to give: the manual says not to work in the prover at first - absolutely do.  In fact, just starting out is probably the MOST necessary time to work directly in the prover.  If you try to work out the proof in advance, without knowing the depths of the system, you'll be taking the express route to Hell.