>We've run another search for shorter proofs. There are quite a few and >it's unclear how the group wants to handle them so we decided to >simply dump them so that everyone can get a chance to review them and >pick what they feel is useful.
I'm remote and can't review the files right now, but I think in principle we should simply follow our current rules: - We should normally never add axioms to a non-ALT proof. We should try to remove Axiom use, especially the Axiom of choice. During this persistently overtime reduces the number of axioms all theorems depend on, even indirectly. - If there is a proof that uses more axioms but is significantly shorter, we often add them as ALT theorems. When in doubt, I think we should add them as alt theorems. Not everyone cares about minimizing the number of axioms, and the full use of axioms can produce much clearer and shorter proofs. - We normally do not keep longer proofs unless they demonstrate something important. But if you see a longer proof that should be kept, make it an ALT proof. We have version control, so we can always restore something later if desired. - Whoever does significant shortening should be credited, e.g., "(Shortened by OpenAI)". it may take a little time to process a lot of results, but I see that as a very happy problem. --- David A.Wheeler -- 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/48409F54-E0BD-4D51-A623-22D5BC074251%40dwheeler.com.
