OpenAI: proofs of some unproven assertions of set.mm.

[augustepoiroux]

As suggested by @david-a-wheeler , we (OpenAI @spolu ) ran our model on some of the unproven statement in set.mm. This PR proposes a few proofs we found:

• lt2sqtROY by Roy F. Longton
• ntrivcvgcaulem1 @sctfn
• axpowndNEWlem1 @nmegill
• bj-inrab3 @benjub
• sqrltROY by Roy F. Longton
• fltsval1 by @glacode (Glauco Siliprandi)
• gsummptadd @david-a-wheeler
• rntrclfv by Richard Penner
• zfcndpowNEW @nmegill

The model also detected that some are already proven under another name

• sqr2gt1lt2ROY -> sqrt2gt1lt2
• relogbcl is set twice
• dfoprab2f -> dfoprab2
• alephprc2 -> alephprc

[nmegill]

The Travis failures were:

?Warning: Line number 110099 ends with a space character, which is discouraged.
...etc...

This check was added recently to prevent frustrating diffs (I know we can use -Z but not all scripts do that). The fix should be easy.

?Warning: Line number 374567 has 81 characters (should have 79 or less):
( cn wcel w3a wne clt wbr wa caddc co c2 cexp cv jca cuz wral cz w...
...etc...

When this occurs in proofs, it can be solved with the command 'save proof */compressed/fast' in metamath.exe.

?Warning: There is no "(Contributed by...)" in the comment above statement
32029, label "zfcndpowNEW".
...etc...

If the contributor is OpenAI, this can be solved by adding "(Contributed by OpenAI, 7-Jul-2020.)" to the comment (usually at the end, but anywhere in the comment will do).

[augustepoiroux]

The Travis failures were:

?Warning: Line number 110099 ends with a space character, which is discouraged.
...etc...

This check was added recently to prevent frustrating diffs (I know we can use -Z but not all scripts do that). The fix should be easy.

?Warning: Line number 374567 has 81 characters (should have 79 or less):
( cn wcel w3a wne clt wbr wa caddc co c2 cexp cv jca cuz wral cz w...
...etc...

When this occurs in proofs, it can be solved with the command 'save proof */compressed/fast' in metamath.exe.

?Warning: There is no "(Contributed by...)" in the comment above statement
32029, label "zfcndpowNEW".
...etc...

If the contributor is OpenAI, this can be solved by adding "(Contributed by OpenAI, 7-Jul-2020.)" to the comment (usually at the end, but anywhere in the comment will do).

Thank you very much! I just corrected those mistakes, hoping I didn't leave any out.

[avekens]

I think this PR must be reviewed very carefully, and a revision is absolutely necessary. Most of the theorems have no comments, and their meaning is not clear. As long as the theorems are in mathboxes, this does not matter (the owner can revise/remove them), but for the main body we must be restrictive, assuring quality.

[arpie-steele]

@avekens I see what you mean.

In some cases a comment appears in @( @) brackets which is, I believe, not notation from the metamath book but intended for humans who are trying to nest comments inside of commented-out blocks. I am however grateful for the proof of rntrclfv and look forward to seeing the eventual paper with the methods.

[spolu]

@avekens \o/ (working on it)

[arpie-steele]

Review
I majored in physics, and would not be anyone first pick to assist in grading, but I thought I would offer some concrete comments on why I think @avekens would request that this PR be canceled or revised extensively before merge.

ntrivcvgcaulem1 adds a distinct variable condition between x and X which is exactly what the original proof was deliberately avoiding.
0/5 Considered Harmful to machine-readable intent.

zfcndpowNEW needs a description. The original, zfcndpow, is based on special theorems. The fact that you short circuit back to ax-pow eliminates its utility in that "conditionless ZFC scheme".
1/5 Considered Harmful to human intent.

fltsval1 needs a description. Perhaps “Extract three parts of the hypothesis.” but begs the question, for what reason would one bundle so many conjunctions in a singular hypothesis when deduction style is normally to have many simple hypotheses. This I expect the "improve all" + "min all" of metamath to do largely for me.
3/5 OK CS work of no known utility.

From the context it looks like axpowndNEWlem1 and fltsval1 remain commented out which begs the question of why prove anything?
4/5 Fine CS work, but low utility.

lt2sqtROY is a repackaging of lt2msq, so could have the same description Two nonnegative numbers compare the same as their squares." Also, you have "Proved by OpenAI" when "Revised by OpenAI" and "Proof shortened by OpenAI" are more common ways to update the proof.
4/5 Fine CS work, but low utility.

Similar comments apply to sqrltROY which appears to be a repackaging of sqrlt; gsummptadd and gsummptfidmadd.
4/5 Fine CS work, but low utility.

bj-inrab3 and rntrclfv look fine to me.
5/5 Looks like real help.

[augustepoiroux]

Review
I majored in physics, and would not be anyone first pick to assist in grading, but I thought I would offer some concrete comments on why I think @avekens would request that this PR be canceled or revised extensively before merge.

ntrivcvgcaulem1 adds a distinct variable condition between x and X which is exactly what the original proof was deliberately avoiding.
0/5 Considered Harmful to machine-readable intent.

zfcndpowNEW needs a description. The original, zfcndpow, is based on special theorems. The fact that you short circuit back to ax-pow eliminates its utility in that "conditionless ZFC scheme".
1/5 Considered Harmful to human intent.

fltsval1 needs a description. Perhaps “Extract three parts of the hypothesis.” but begs the question, for what reason would one bundle so many conjunctions in a singular hypothesis when deduction style is normally to have many simple hypotheses. This I expect the "improve all" + "min all" of metamath to do largely for me.
3/5 OK CS work of no known utility.

From the context it looks like axpowndNEWlem1 and fltsval1 remain commented out which begs the question of why prove anything?
4/5 Fine CS work, but low utility.

lt2sqtROY is a repackaging of lt2msq, so could have the same description Two nonnegative numbers compare the same as their squares." Also, you have "Proved by OpenAI" when "Revised by OpenAI" and "Proof shortened by OpenAI" are more common ways to update the proof.
4/5 Fine CS work, but low utility.

Similar comments apply to sqrltROY which appears to be a repackaging of sqrlt; gsummptadd and gsummptfidmadd.
4/5 Fine CS work, but low utility.

bj-inrab3 and rntrclfv look fine to me.
5/5 Looks like real help.

Thank you very much for this review!
Indeed the proof for ntrivcvgcaulem1 does not respect the condition of discrete variables. The proof for zfcndpowNEW is also not acceptable. These two proofs are now withdrawn.
Some "Proved by OpenAI" have also been modified.

[avekens]

Here my remarks on the (remaining) theorems. In summary, I think only the two theorem of BJ's and RP's mathboxes should be kept (if the owners of these mathboxes agree).

• axpowndNEWlem1 @nmegill
  ** it makes no sence to provide a lemma without correspondig theorem (axpowndNEW)
• bj-inrab3 @benjub
  ** BJ's mathbox, so he should decide
• lt2sqtROY, sqrltROY by Roy F. Longton
  ** The whole subsection "Calculus \ Version of 10-Aug-2005 Roy F. Longton \ 9-Sep-2005 neighex added" is commented out - it makes no sense to prove/provide only two of the (many) theorems of this section. In addition, this is part of section "(Future - to be reviewed and classified)", which is strange enough...
• fltsval1 by @glacode (Glauco Siliprandi)
  ** The whole section "Fermat's Last Theorem" is commented out - it makes no sense to prove/provide a single of the (many) theorems of this section
• gsummptadd @david-a-wheeler
  ** there is no added value of this theorem compared with gsummptfidmadd used in its proof
• rntrclfv by Richard Penner
  ** RP's mathbox, so he should decide

[glacode]

Hi Auguste,

fltsval1 shouldn't be in my mathbox (I'm pretty sure I've never had unproven theorems in my mathbox).

In my local set.mm version (it's not up to date) fltsval1 is in a section for the Fermat's Last Theorem

Glauco

[benjub]

I've only had time to look at ~bj-inrab3 and it looks good to me. Congratulations to @spolu and @augustepoiroux .

[nmegill]

I have added an empty mathbox for OpenAI in PR #1712 (search for "Mathbox for OpenAI" in set.mm). You should be able to merge it with this PR without conflict.

Normally, contributions by OpenAI other than proof shortenings should initially go into a mathbox specifically for OpenAI instead of being edited directly into the main part of set.mm. There is more freedom in terms of what you can do in your mathbox, as opposed to the main part of set.mm which is vetted carefully for certain conventions to maintain quality. Over time we may decide to move useful theorems from the OpenAI mathbox to the main part of set.mm.

By the way the conventions we follow are described here:
http://us.metamath.org/mpeuni/conventions.html

Comments on the specific changes in this PR:

axpowndNEWlem1 - this does not seem to shorten the original proof, and worse it makes the theorem no longer useful by introducing a $d. I think it should be deleted (or at least moved to the OpenAI mathbox if you want to keep it).

fltsval1 - as has been mentioned, this theorem was commented out and wasn't intended to be used. The whole commented-out section called "Fermat's last theorem" should have been deleted a long time ago but was overlooked, and I think now is the time to delete it to prevent further confusion. (I am puzzled as to why this was chosen by OpenAI since it is just a comment; I assume OpenAI recognizes the comment syntax? If it was chosen manually, maybe syntax highlighting in the editor would prevent accidentally using a commented-out theorem.) The proof can be moved to the OpenAI mathbox if you want to keep it, but I will delete that whole section in the next few days.

lt2sqtROY, sqrltROY, - same issue: this is in a commented-out section that hasn't been maintained since 2005, and it should have been deleted a long time ago since it will never be used. Again I will delete that section in the next few days, so if you want to keep the proofs they should be moved to the OpenAI mathbox.

gsummptadd - This was commented out in TA's mathbox and appears to be superceded by gsummptfidmadd, so might become deleted (TA can decide that). Keep in mind that work inside of other people's mathboxes is often work in progress, and it is generally advisable to coordinate any work there with the mathbox owner.

bj-inrab3, rntrclfv - Again, these were commented out theorems in others' mathboxes; the mathbox owners can decide the disposition.

[augustepoiroux]

Thanks to @avekens and @nmegill for your comments! We fully understand your points of view. Appropriate changes will be made.

Thank you for the Mathbox!

[augustepoiroux]

To go back to why we proposed these proofs:
The idea, first suggested by Thierry Arnoux (https://groups.google.com/d/msgid/metamath/531b6980-d1ba-e90f-a47d-c0830bc709cb%40gmx.net), was to try to prove, with the OpenAI model, unproven theorems found in set.mm. This allows us to see how the model behaves on theorems it has never seen. Then we decided to share the proofs we found here. Next time we'll do that in the OpenAI's Mathbox as suggested.
Also, the modifications suggested for this PR have been applied 😃

[tirix]

I'm coming after the battle...

I probably needed ~ gsummptadd in one of my work in progress at some point in time (March '18 it seems), but found a better solution later on which did not require it anymore, and kept the theorem statement in comments as it was still a valid useful statement which would need to be proven sooner or later. Then came Alexander who proved it and named it differently, ~ gsummptfidmadd. I'll delete the commented out statement.

How about ~ gsummptres , which is in the comment right afterwards, did OpenAI manage to find a proof?
There does not seem to be any exactly matching theorem from Alexander, but ~ gsummptfidmsplit would bring you a long way. Is there any way to suggest to OpenAI to use this?
I have not used the OpenAI-based proof assistant yet, maybe I'll give it a try with that.