Moreover Wheeler's idea of adding non-minimized proofs could be applied systematically in these sections. They would then constitute genuine material for the training of a minimization engine based on artificial intelligence. The material would be abundant and well delineated in set.mm so that it could be easily identified if it is to be removed or minimized later.
-- FL -- 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/eae2c591-3838-423c-acb3-63b5b0936e26o%40googlegroups.com.
