Abandoned work

[wlammen]

Slowly, but inevitably, we will see more and more work in our databases like set.mm, that is not maintained any more, like mathboxes. The reason why maintenance has stopped could be: lost interest in mathematics, or Metamath in particular, basic changes in life consuming time (like children), or, horrible dictu, simply death. Currently, the amount of abandoned work has not accumulated to a degree that calls for immediate action, in my eyes. Nevertheless I am curious how you think about this topic. Should we in preparation for upcoming years develop rules by which we formally decide when to remove something apparently abandoned from the repositories? Or are ad hoc decisions sufficient, in case something becomes urgent enough? Looking forward to your opinions.

[jkingdon]

In many cases it is a candidate for moving out of mathboxes. We're pretty good at doing that theorem-by-theorem, and perhaps existing rules like "move it if someone wants to use it for another proof" will help give us an idea of when to do this.

Of course a Metamath 100 theorem, or something of similar importance, should not be removed. It should be either maintained in place as we need to (since some kinds of set.mm-wide changes are fine even across mathboxes) or moved out of mathboxes.

[david-a-wheeler]

I don't see a strong reason to remove such work, as long as it's still proven correct. Work by others from years ago may form the foundation of future work; you could even argue that all of mathematics is like that.

As far as "rules" go, I think anything in the Metamath 100 (and their dependencies) should eventually be moved into the main body. By definition someone thought the results were important in a broader way, and they're being referenced externally.