In the past, every year or two we would run "minimize_with" on the entire set.mm. But as set.mm has grown, doing this has become a somewhat large project. The last time was in Feb., which involved people volunteering their CPUs over several weeks as well as my time managing it.
Benoît suggested that we require proofs to be minimized before submission. This would make a global minimization a lower priority effort that we could do less frequently. (Benoît's suggestion was motivated by noticing a proof that was shortened manually in the same way that "minimize_with" would have done automatically, accompanied by a "Proof shortened by" credit and a *OLD version.) However, I tried making it a requirement a decade or so ago without much success. Sometimes contributors would agree but sometimes forget to do it, and one person objected that it was too much effort. So while we would like contributors to minimize their proofs before submission, it's not something practical to expect or enforce. I propose we add a temporary tag to recent set.mm proofs that lets us know whether or not "minimize_with" has been run. Volunteers can, at their leisure, minimize the proofs that haven't been. Ideally we would have a tag or marker in the comment like "(Minimization pending.)", or maybe just "(*)" to minimize clutter, indicating that a proof hasn't been minimized. The volunteer would delete this marker after minimization. To start with, I would put the marker in every theorem added since Mar. 5, 2020 (when the last full minimization was run). Then we would expect all contributors to put this marker in future contributions, whenever they haven't minimized their submitted proofs. A problem with this is that it is hard to enforce putting in a "minimization pending" marker in new theorems - people will simply forget to do it - and "verify markup" has no way of detecting whether or not a proof was really minimized. So maybe we need two markers standing for "minimization pending" and "minimization done". All "minimization done" markers would be deleted after a period of time like a year (we don't want them in set.mm permanently since they add no value). "verify markup" could then produce a warning for recent theorems (< 1 year old) that have neither marker. This seems a little inelegant, but I couldn't think of another way that "verify markup" could recognize. (Whatever we decide, I could add some automation in metamath.exe to update the marker when a proof is minimized.) I'd like to hear opinions or suggestions. Norm -- 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/e8304e5d-22bd-4f29-8099-319166e88ac6n%40googlegroups.com.
