More proof shortenings from OpenAI's models

[Stanislas Polu]

Hi!

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.

They're not all directly applicable (some are artifacts of old
versions of theorems remaining in people's Mathbox) but many of them
seem quite interesting. Note that we filtered all shortenings of *ALT
or *OLD because they generally use their alternate, and kept only the
proofs that were shortened by a factor of at least 2x (so if there is
a need for it, we can get more).

You'll find two files attached, which is an artifact of how we split
the database between a train and held-out test set but each file is
roughly ordered by appearance in set.mm.

Some notable examples I've spotted in test.shortening:

- `1re` uses more axioms but is much simpler (how do we feel about
that given the comment there?).
- `dvtanlem` is probably the most epic shortening (247 steps to 14).
- `elmod2` is quite nicely simplified.
- `elsb4` and `reean` I believe are not only shorter but also have a
smaller axiomatic trace.

Hope this is useful to the community!

-stan

[David A. Wheeler]

>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

[ookami]

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

[Glauco]

Additional distinct variable conditions can really weaken results (and / or make theorems much more difficult to use)

Glauco

[Stanislas Polu]

Totally agreed that we should be very cautious with these shortenings.
We shared these dumps with the community because it would take us a
lot of time to apply the level of care required to each of these
theorems yet believe that they can also be useful as is.

We'll look into filtering the proofs that are safe to apply directly
(no extra DVs and lowered or equivalent axiom trace), as this subset
may be more useful to tackle first.

-stan

> --
> 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 metamath+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e2456dbb-8950-4d0f-85c1-98934557ee16o%40googlegroups.com.

[Alexander van der Vekens]

Hi Stan,
very interesing results. I had a look at the theorems I contributed in test.shortening:

• ~reuan: Additional distinct variable condition! This shortening must not be performed.
• ~elmod2: This shortening is great! It should be done in set.mm
• ~el2fzo: To be investigated if this theorem is still useful (or if its single usage can be replaced by elfzolt3b found by the shortening).

I had only a quick glance at train.shortening (what is it good for?) - it seems to be a lot of good shortenings in there, too.

For ~suppss2f, however, the shortening is not allowed, because an OLD theorem (suppss2OLD) is used for it. And the shortening of ~ subdir2d shows that it is a duplicate of ~subdid.

Regards,

Alexander

[Stanislas Polu]

Hi Alexander,

Thanks a lot for looking into this!

The test.shortening/train.shortening is a quite arbitrary split
(shortenings coming from the training set vs the test set we use),
both are to be considered.

Best,

-stan

> --
> 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 metamath+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9f2536d7-d120-41e3-ba3d-9802270a9f69o%40googlegroups.com.

[Norman Megill]

This is nice work Stanislas, thank you.

On Friday, July 3, 2020 at 5:09:55 AM UTC-4, Stanislas Polu wrote:

- `1re` uses more axioms but is much simpler (how do we feel about
that given the comment there?).

A problem with this particular proof is that it uses df-1, which has the tag "(New usage is discouraged.)".

Let me explain a little about how the complex numbers are introduced.  Our overall goal in set.mm is to show mathematics that follows from the ZFC axioms.  For complex numbers, we construct a model (a set of axioms stated as $p statements) starting from ZFC axioms.  We then restate these derived axioms ($p statements) as actual axioms ($a statements) in order to (1) make the complex number development independent from the construction (so that alternate models could in principle be "plugged in") and (2) make it easier to see what complex number axioms are needed for a particular complex number theorem.  So, for example, we derive ax1cn in the model part, then restate that theorem as axiom ax-1cn.  (To help ensure we're not cheating by introducing new axioms beyond ZFC, the 'verify markup' command in metamath.exe checks that each ax-* $a statement exactly matches an earlier $p statement with the "-" removed, if such a $p statement exists.)

To help prevent the accidental usage of the complex number construction when we later use complex numbers, we have "(New usage is discouraged.)" in every statement in the development of the complex number model.  df-1 is one such statement, since it might change if we used a different complex number construction.

For our metamath.exe and mmj2 proof assistants, the string "(New usage is discouraged.)" in a comment tells the proof assistant not to consider that statement for use in a proof being developed.  In addition, the Travis run that is done after each pull request checks that the usage of statements with "(New usage is discouraged.)" didn't change as a result of the PR (unless it was done intentionally and the user has supplied a regenerated "discouraged" file as part of the PR).

I would recommend that the OpenAI assistant check statement descriptions for the string "(New usage is discouraged.)" and avoid considering them for use in proofs.  (The metamath.exe command 'write source set.mm /rewrap' currently prevents this string from being broken across lines, but I'm not sure we want to guarantee that, nor can we guarantee the '/rewrap' command was run.  But for a quick and dirty check you can assume it's not broken across lines and refine it later with a TODO.)

Norm

[Stanislas Polu]

Hi Norm,

That's extremely helpful. We will look into enforcing discourage uses
in the future, to shorten the loop between our models and set.mm.

Thank you very much.

-stan

> --
> 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 metamath+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dd8ea31b-8799-4591-a6d4-688c519eedado%40googlegroups.com.

[Alexander van der Vekens]

Hi Stan,

with PR #1715, the proofs of the following theorems are replaced by the proofs shortened by OpenAI for the following theorems (taken from test.shortening):

• ndmima
• relcoi1
• cmntrcld
• dvtanlem
• dvdsabsmod0
• elmod2
• xphe

el2fzo was removed (see my previous comment).

Alexander

[Stanislas Polu]

Thank you so much for looking into this.

-stan

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c2970a38-da10-4185-a25d-c3f2c3b26a70o%40googlegroups.com.