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.
