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 On Mon, Sep 7, 2020 at 7:00 PM Norman Megill <[email protected]> wrote: > 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 > > On Monday, September 7, 2020 at 5:17:17 AM UTC-4 ginx wrote: > >> 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. >> >> >> >> >> >> >> >> >> >> >> >> >> > > > > > > > > -- > > > 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/e0364c41-9804-43fe-8117-b796a73a242an%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/e0364c41-9804-43fe-8117-b796a73a242an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > > -- 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/CACZd_0wcMjxJ_G%2Bc3TD5%2B4O9RdvdfHXR%2Bh5N5KnNWT63gqw7UA%40mail.gmail.com.
