Mathboxes no longer maintained

[wlammen]

Pull request #4528 modifies Norm Megill's mathbox. In my eyes it is a move for the better, but it breaks with some ideas around mathboxes. I think of a mathbox as a private area, where you can develop your own ideas, visible to all. Others have a chance to comment on them, or use the results as a repository for theorems (move to Main), but not much more.

Extracting a theorem, and moving it to Main is, as far as I know, the only way to essentially modify a mathbox without consent of its owner.

How shall we deal with mathboxes that are knowingly abandoned (as is the case with NM's one), or where the owner hasn't shown up for several years? How can we avoid garbage in the long run, due to missing maintainance, without compromising the idea of privateness? In reviews I generally accept material for mathboxes that I haven't understood fully. This is helpful for development, but has the risk to add unsustainable contents.

What do you think about this? Let me know here in your comments.

[GinoGiotto]

From what I can tell, a mathbox owned by a deceased individual should be promoted to have the same rules as main. Since the owner no longer has control over it, there is nothing left to do other than letting other maintainers do the job, and such job should be aligned with the established rules for main. To me, this is the most logical way to approach it.

[avekens]

I think we should discuss the special case of #4528 within issue #4265 which was opened exactly for this case.

In general, we have already rules how to maintain mathboxes: proofs (without "(Proof modification is discouraged.)") can be changed (modified, simplified, shortened), label changes (and other changes in main) must be respected - all without the need to ask the mathbox owner. And, of course, moving things to main, as explained above. Nothing else should be done with mathboxes. And there is no need to add a "(New usage is discouraged.)" tag for a theorem in a mathbox (as done in #4265), because it must not be used outside the mathbox anyway.

[jkingdon]

If we are changing df-riota we should change mathboxes accordingly. This isn't a new idea. Here's the text from https://us.metamath.org/mpeuni/mathbox.html :

Even though in a sense your mathbox belongs to you,
it is still part of the shared body of knowledge contained in set.mm,
and occasionally other people may make maintenance edits to your mathbox
for things like keeping it synchronized with the rest of set.mm,
reducing proof lengths, moving your theorems to the main part of set.mm
when needed, and fixing typos or other errors.

I grabbed the text from 2021 although I don't think it has changed since then.

As for the details of exactly what changed related to df-riota I haven't been following that closely enough to comment, but if we are making a global change it can be across both main and all mathboxes.

So that's for the kinds of edits which can be made across mathboxes. What about unmaintained mathboxes in particular? Our guideline on that is a bit more recent than the above but as far as I can tell gives us a decent idea of how to proceed:

If a contributor is no longer active, we will continue the usual maintenance edits. As time goes on, often theorems will be moved to main or removed in favor of similar replacements. But we are also willing to maintain mathboxes in place, as work by others from years ago may form the foundation of future work; you could even argue that all of mathematics is like that.

(that's from further down mathbox.html)