I agree that minimization markers "add no value", so in my opinion they should be kept out of set.mm altogether. Maybe we can create a file "minimized_theorems" (something like "discouraged") which will be a list of, well, minimized theorems :-) Contributors won't have to set any tags or modify that file, but if someone decides to minimize a theorem, they will check that file and in case if the theorem wasn't processed earlier they will minimize it and add the name to the file. That way we will avoid additional bureaucratic burden of contributing to set.mm.
The "minimize" command of metamath.exe can be made to skip minimization of theorems mentioned in the "minimized_theorems" file, so minimization volunteers will be able to minimize whole ranges of theorems in bulk, without doing double work. And speaking of making users minimize their theorems, I think most people need only a small reminder. Right now, after you complete a proof in metamath.exe, the program will remind you to do "SAVE NEW_PROOF" and "VERIFY PROOF". Perhaps a suggestion to minimize the proof can be added there as well? Same goes for mmj2, after a proof is finished and mmj2 compiles it to the compressed proof format, one can add an automatic comment suggesting the user to run "minimize" in metamath.exe. -- 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/cb2e2d8a-4a02-4240-986d-b63132c485f5n%40googlegroups.com.
