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). El martes, 8 de septiembre de 2020 a la(s) 10:59:42 UTC-5, [email protected] escribió: > 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. > > > On September 8, 2020 3:09:35 AM PDT, "[email protected]" < > [email protected]> wrote: >> >> 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 <https://github.com/metamath/metamath-exe> or mmj2 >> <https://github.com/digama0/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 >> <http://us.metamath.org/downloads/metamath.pdf>, watch David's videos >> <https://www.youtube.com/watch?v=Rst2hZpWUbU&t=2s> and then do Filip's nice >> problems <http://us.metamath.org/mpeuni/mmtheorems300.html#mm29972b>. >> 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 >> <https://docs.google.com/document/d/1cpbz2ZJ60qR0220fUTvCWAv4NYX4y8JTClCwGnzryXc/edit?usp=sharing> >> >> are the problems I have done with it to help in case you get stuck, though >> I am not so expert. >> >> Jon >> >> On Tuesday, September 8, 2020 at 4:14:38 AM UTC+1 David A. Wheeler wrote: >> >>> On Tue, 8 Sep 2020 10:31:37 +0800, Thierry Arnoux <[email protected]> >>> 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 >> >> -- 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/75681fd1-3e68-491b-9cca-5a4846269c6dn%40googlegroups.com.
