On Wed, Sep 9, 2020 at 5:58 PM Norman Megill <[email protected]> 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 <[email protected]> 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 -- 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/CAFXXJSsrdRr0dfYdbvdsdX0rrW_UKQghtBjdvj6wRigEQYuFuA%40mail.gmail.com.
