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
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