As a sort of opposite opinion, I would like to argue that the current convention of moving theorems out of mathboxes (move only if it's used by someone else) should also apply to metamath 100 results.
First of all, metamath 100 theorems are clearly not obscure facts that are hard to find, they are announced in the google group, showcased in the "recent news" on the metamath site and also permanently linked in the metamath 100 list. Now, if some metamath 100 theorem required the development of an important branch of math currently missing from set.mm (matrices or Fourier series, among recent examples), then it should be relatively easy for someone to make use of those theorems and fulfill the current movement criterion. Needless to say, another person might uncover some problem or inconvenience in the new math section, overlooked by the metamath 100 contributor. In case new theorems are not being used, they can stay in the mathbox without any trouble, in my opinion. It gives the author more time to improve his results, and ultimately can't make them worse. I must agree that theorems in the main body of set.mm are more "well-known" than mathbox results, but I think that the "hype" around metamath 100 theorems is high enough to make people remember where to look if they want to prove something about matrices or Fourier series :-) As a compromise suggestion, maybe instead of deliberately moving all metamath 100 results into the main body we shall leave it to the contributor of the corresponding theorem? I.e. allow them to move their metamath 100 entry into the main part when (or if) they want. And in case someone wants to see a metamath 100 theorem formalized by another person in the main part, they can always come up with some theorem using the metamath 100 result in question to formally satisfy the movement "rule" :-) -- 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/936fa710-ca8b-4055-82f0-0b1fc228c178%40googlegroups.com.
