On Mon, 30 Dec 2019 00:58:45 -0800 (PST), savask <[email protected]> wrote: > 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.
it's true that the metamath 100 final results are not "obscure". However, all the supporting material in mathboxes is *much* less visible than material in the main body. Their primarily heading level is the name of a person, instead of their logical position, and in many cases tools ignore those theorems by default. The "mathbox" construct is very useful. I just think there's a lot of material in the mathboxes today that should move into the main body. Different people have different specializations, so not all material that should be in the main body will "naturally" move up through the "use by two people" rule-of-thumb. I don't think it needs to be complicated, or have an additional "stage". If you see stuff in your mathbox that you think is ready to move into the main body, please make pull request(s) that moves groups of that work into logical places. Some requests will get some pushback, and others will be "sure, that makes sense". ... > 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? In general I agree with that, in the sense that the person who created the proof probably has additional insight into "where it goes" in the main body. But I want to encourage people to do so. Not all such proposals will be accepted, but then there can be a reasonable discussion. --- 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/E1ilyRt-0000b2-9b%40rmmprod07.runbox.
