Hi ginx! Welcome to the community! It’s perfectly fine to use this group for an introduction and as a call for help! It sounds like Metamath is a great idea for a graduation project.
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. Which area of the mathematics are you more interested in? I would recommend a domain where you feel comfortable, so that not both the Maths and the Metamath are new. So besides the 100 theorems, you might also look at Math theorems you have learnt in your CS curriculum and which might not have been formalized yet. Again, welcome, and I wish you a lot of fun! BR, _ Thierry > Le 8 sept. 2020 à 09:18, David A. Wheeler <[email protected]> a écrit : > > On Mon, 7 Sep 2020 14:23:41 -0700 (PDT), Norman Megill <[email protected]> > wrote: >>> 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. >> It looks like Google stripped the leading spaces from the python program. >> @David, did you save this program, and if so could you run it for us to get >> an updated list? Thanks. > > I didn't save the code, but it was easy to reconstruct its indentation. > I also tweaked it to make its results prettier. > > Here are the results: > > 4 6. Gödel's Incompleteness Theorem > 3 84. Morley's Theorem > 3 40. Minkowski's Fundamental Theorem > 3 36. Brouwer Fixed Point Theorem > 3 28. Pascal's Hexagon Theorem > 3 13. Polyhedron Formula > 3 100. Descartes Rule of Signs > 2 99. Buffon Needle Problem > 2 8. The Impossibility of Trisecting the Angle and Doubling the Cube > 2 53. Pi is Transcendental > 2 29. Feuerbach's Theorem > 2 12. The Independence of the Parallel Postulate > 1 92. Pick's Theorem > 1 56. The Hermite-Lindemann Transcendence Theorem > 1 50. The Number of Platonic Solids > 1 47. The Central Limit Theorem > 1 41. Puiseux's Theorem > 1 32. <u>The Four Color Problem</u> > 1 21. <u>Green's Theorem</u> > 0 82. Dissection of Cubes (J.E. Littlewood's "elegant" proof) > 0 62. <i>Fair Games Theorem</i> > 0 59. <i>The Laws of Large Numbers</i> > 0 43. <i><u>The Isoperimetric Theorem</u></i> > 0 33. <i><u>Fermat's Last Theorem</u></i> > 0 24. <u>The Undecidability of the Continuum Hypothesis</u> > 0 16. <i>Insolvability of General Higher Degree Equations</i> > > This is only an *estimate* of current achievability, of course. > I'd love to hear comments of where people think the theorem is > more or less achievable given the start of set.mm. > > I'll create a pull request to add this script to the scripts subdirectory. > > Aside: I created an indentation-sensitive syntax for Lisp, called Sweet > Expressions, > which supports "!" as an indent character. Among other things that > prevents this "gobbling" of leading whitespace. > > --- 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/E1kFSHG-0006Uy-LF%40rmmprod06.runbox. -- 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/221EED5B-F4BC-4C39-8512-59B92F570465%40gmx.net.
