> On Dec 11, 2020, at 10:13 PM, Norman Megill <[email protected]> wrote: > > Benoît suggested that we require proofs to be minimized before submission.
I think we should encourage that. I think requiring is too strong, but simply making that request clear is reasonable enough. > 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. .,.. > I'd like to hear opinions or suggestions. I disagree. It does not really help. Minimization is often enabled by adding something *else* later, so such tags would be misleading. In addition, adding them would be a pain & create a lot of useless fluff. > 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. To me the solution is clear: automation. When we started last time almost nothing was automated. I ended up writing some scripts to automate parts of it, but that was done on the fly *during* the minimization. Instead, let’s play on letting the computers do all the work. If it’s going to happen annually, then let’s treat it as something that automatically happens annually. --- 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/8A24496B-3658-4DFA-8C38-4742145BE14F%40dwheeler.com.
