> > ... > 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. >
I fully agree that mathboxes material is not that often looked at, but it's not hidden in any way either. If someone is eager to contribute to set.mm, they will surely find about mathboxes and material in there. As for tools ignoring mathbox theorems, it's a problem of our proof assistants not of set.mm organization, in my opinion. 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. > My point is, if the material is not going to be used by anyone but the author, is it worth moving it into the main part? If someone were, for instance, to formalize the four color problem in metamath, would it be worth putting such a piece of highly specialized mathematics into the main body of set.mm? Of course it's a stretch, but in my opinion if the area is important (and, so to say, fundamental) enough, it should be relatively easy to fulfill the current movement rule. For example, that also settles the tooling question: if you suffer from your proof assistant not suggesting mathbox theorems, then you've found a good use for those theorems, and they can be happily moved into the main body. 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". > That is, perhaps, my main concern. The current rule leaves almost no place for objections or disputes, while the idea of something "being ready to be in the main body" is quite broad. There might be different views on how certain conceptions should be formalized, and I think the most fair way to rule out such situations is by showing your support: if someone but the author is eager to use new results and conceptions then they are not useless and accepted by, at least, two people. I agree that often it's favorable to move some mathbox results into the main part without waiting for someone to utilize them, but I don't think it should be done often. Metamath 100 contributions indeed frequently touch important math areas and I fully support the idea of moving these "chunks" of theory into the main body (if the respective contributor is okay with that), but I'm not sure if the same practice should be adopted for other seemingly important results. -- 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/18b74de1-f9fd-4b3c-a75b-4aafb5c37103%40googlegroups.com.
