> On Feb 16, 2023, at 4:14 PM, Igor Ieskov <[email protected]> wrote:
>
> > 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.
I suggest creating multiple pull requests. That way we can easily accept some &
not others.
> 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
That's fine, we know who they are. To be fair,
their public names are a terribly-kept secret, since they're posted in
<https://us.metamath.org/metamath/set.mm>.
If someone doesn't want to give their real name they can just give their
pseudonym (e.g., Mel L. O'Cat, Drahflow) or abbreviation (KP, ML),
though real names are great because I expect this database to outlive all of us.
--- 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/280338AA-0B0B-446C-BCA1-30FE76710954%40dwheeler.com.
