*> Would you mind taking some steps so we can more easily review & add them?*
Sure. I've just created a pull request. I will gradually update proofs from the main part. I will not touch proofs from mathboxes. Below I am providing a list of owners of mathboxes for which I found shorter proofs in order others not to download the file I attached (not sure if posting full names is a good idea): AS AV GS JB NM RP TA WL - Igor On Thursday, February 16, 2023 at 6:14:32 PM UTC+1 Alexander van der Vekens wrote: > 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. > > OLD theorems will be removed after one year, so shorten their proofs is > useless. > -- 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/aecd946f-4657-430c-8bb4-f6db6bdc4d84n%40googlegroups.com.
