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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e0364c41-9804-43fe-8117-b796a73a242an%40googlegroups.com.
