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.
