> On Feb 16, 2023, at 3:12 AM, Igor Ieskov <[email protected]> wrote:
>
> Hi all,
>
> I found shorter proofs for some theorems in set.mm. They are listed in the
> attached file shorter-proofs.zip. There are 108 theorems, 47 in the main part
> of set.mm, the rest in mathboxes. Some of them are marked as OLD or "proof
> modification is discouraged", but I included such theorems into that file
> anyway. Since I am not sure how useful this result is and because of big
> number of theorems, I verified only the first 5 theorems by metamath.exe. I
> hope new shorter proofs for remaining theorems are also valid, but there is a
> chance that some of them are not.
That's awesome!
Would you mind taking some steps so we can more easily review & add them?
We normally accept changes using git & GitHub. That process will automatically
check the validity of the proofs in a variety of ways. I suggest breaking your
changes
into multiple changes, so that we can easily accept some while considering
others.
If you don't know how, we can try to help!!
We generally don't change "proof modification is discouraged" so you'll need to
justify
those changes (or drop them). I don't think we officially reject them for
"OLD", but I
wouldn't focus your time on them.
--- 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/3FF44152-DEB1-478F-B0DE-5A1D66A00712%40dwheeler.com.
