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/a12cf68b-57e2-4cff-8bb8-d230818ed629n%40googlegroups.com. -- 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/52F47BF8-BE39-4A38-B381-89A43563DC3E%40panix.com.
