Hmm. elsb4 has an extra distinct variable condition (x and y must be different), which the original theorem does not have. I did not look at the other results, but some care is in order, I think.
Wolf David A. Wheeler schrieb am Freitag, 3. Juli 2020 um 16:02:18 UTC+2: > > >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/93b8b7e0-4232-412d-b88b-037f260a6d0an%40googlegroups.com.
