On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote: > Norm: > > Thanks for the reply, I’m definitely going to hang out around here more > often. The 100 theorems is my ideal option, I was scheming the list > provided and some theorems caught my eye, like the four colors one, > however, that one has only bene proven by Coq, so it might out of hands for > me (at least for the purpose of the dissertation). The Insolvability of > General Higher Degree Equations also caught my eye, but that one is even > worse since it appears to have no formalized proof by prover yet. Descartes > Rule of Signs is one that I’m already familiarized with and 3 provers > already have it so this one could be a good option. > > Other than that, I’ve got a couple of theorems in mind that do not belong > to the 100 theorems. Erdős–Szekeres theorem, Chinese remainder theorem, > Kummer's theorem, Lucas's theorem and others. Or maybe just check the > validity and/or worst time/space complexity of some CS algorithms, such as: > Kosaraju's algorithm, KMP algorithm, Sieve of Eratosthenes (regular one and > linear time one), and others. Maybe even for data structures as well. Main > problem is, I’m not sure which of these have already been solved in > Metamath or are currently being solved. Is there some sort of index to > check for this? > There is an outline of the set.mm content here: http://us.metamath.org/mpeuni/mmtheorems.html although it doesn't always show specific theorems on the Table of Contents page but just the general area covered by a section.
The Erdos–Szekeres theorem and the Chinese remainder theorem are here: http://us.metamath.org/mpeuni/erdsze.html http://us.metamath.org/mpeuni/crt.html You can click on "Nearby theorems" on the above pages to see related material. The small colored number after a theorem label will let you determine where it falls in the mmtheorems.html table of contents. (It looks like erdsze is still in Mario's "mathbox" [which is a work space assigned to individuals for developing proofs - you will get one]. Since it is one of the mm100 theorems, at some point it probably should be moved to an appropriate place in the main body of set.mm.) BTW I found the above theorems by searching set.mm in the metamath program: ./metamath MM> read set.mm MM> search * szek /comment MM> search * chinese /comment Other tools like mmj2 also have search functionality, and worst-case there's grep :) Since Mario did the above 2 proofs, perhaps he has comments on some others on your list, such as to what extent we have the necessary background material developed. Norm -- 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/b7208b72-cdc6-42c8-abc1-fbf0e9ab7967n%40googlegroups.com.
