[Metamath] Re: Proposal for on-going proof minimization

2020-12-13 Thread 'Alexander van der Vekens' via Metamath
Sorry, but maybe my comments were more confusing than helpful for the discussion: On Sunday, December 13, 2020 at 4:54:33 PM UTC+1 Norman Megill wrote: > It looks like my proposal wouldn't be welcomed, so I will abandon it. As > for keeping a list of minimized theorems, I'm not really in

[Metamath] Re: Proposal for on-going proof minimization

2020-12-13 Thread Norman Megill
It looks like my proposal wouldn't be welcomed, so I will abandon it. As for keeping a list of minimized theorems, I'm not really in favor of that either; it would be one more thing to maintain that people will forget or neglect. As for mathboxes, we've never had a rule about people