> 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. >
Well "minimized" not "removed". -- 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/5007999d-79f9-4a07-b68a-6c5a68296226o%40googlegroups.com.
