Shortening of various proofs based on OpenAI's provers

[spolu]

This PR proposes various shorter versions of proofs discovered by automated reasoning models developed at OpenAI.

We focused on proofs that were substantially shortened and not marked as discouraged for modification.

The process was run on a sample of ~1k theorems from set.mm. If there is interest from the community we can probably get ~45 times as many shortened proofs.

(Starting a thread on the group in parallel to discuss this)

[wlammen]

An observation:
ra4 is also reproved by @benjub in his pull request #1548 , and, according to the comment, he reduced the axioms used in the proof. The metrics by which proofs are measured prefers fewer axioms over proof length. So one should carefully decide which version to include finally.
Formal objections:
The former proof is usually kept as an OLD theorem for about a year. By comparison, one can learn from improvements, or simply check that rules are not violated. The OLD files are not included in the pull request, as far as I can see. Also, if the previous proof has been shortened before, the corresponding attribution is kept, instead of being overwritten. This reflects the idea that a shortened proof, while not the final candidate, might still have been a valuable intermediate stage to start from.

Apart from that, I would like to see the results from the AI, and I appreciate your efforts in this respect.

[spolu]

Thanks for your comments! I will update the PR accordingly and will run the analysis of how it impacts axioms dependence. Best,

…

-stan

On Thu, Mar 26, 2020 at 9:16 PM, wlammen ***@***.***> wrote: An observation: ra4 is also reproved by ***@***.***(https://github.com/benjub) in his pull request [#1548](#1548) , and, according to the comment, he reduced the axioms used in the proof. The metrics by which proofs are measured prefers fewer axioms over proof length. So one should carefully decide which version to include finally. Formal objections: The former proof is usually kept as an OLD theorem for about a year. By comparison, one can learn from improvements, or simply check that rules are not violated. The OLD files are not included in the pull request, as far as I can see. Also, if the previous proof has been shortened before, the corresponding attribution is kept, instead of being overwritten. This reflects the idea that a shortened proof, while not the final candidate, might still have been a valuable intermediate stage to start from. Apart from that, I would like to see the results from the AI, and I appreciate your efforts in this respect. — You are receiving this because you authored the thread. Reply to this email directly, [view it on GitHub](#1547 (comment)), or [unsubscribe](https://github.com/notifications/unsubscribe-auth/AAADVW2XJM6HS25ZEIKXT73RJOZYJANCNFSM4LULMKNQ).

[nmegill]

I think that PR #1548 (which I accepted ahead of yours pending your anticipated PR changes) also made changes to ra4, and I believe this is causing the merge conflict. Perhaps it is best to restore the original ra4 (or use the #1548 version) and we can decide what to do later.

[benjub]

Actually, I only changed the comment of ra4, and I added a new theorem ra4v (a trivial change: ra4v uses stdpc5v where ra4 uses stdpc5). The new proof found by @spolu's AI is actually different, so that ra4v will not be a trivial adaptation of ra4 anymore. I think that's not a problem: @spolu should go ahead and keep the current proof as ra4OLD.

[spolu]

@nmegill as per the associated email thread; I propose I assess the impact on the axioms referenced by each theorem.

For the ones where we don’t use more axioms I will rename the current proofs as *OLD and replace; otherwise I’ll introduce the new proof as *ALT.

If that‘s ok with you?

[nmegill]

For the ones where we don’t use more axioms I will rename the current proofs as *OLD and replace; otherwise I’ll introduce the new proof as *ALT.

I think *ALTs are OK, at least at the beginning of this project, because of the interest and novelty factor. If we end up with hundreds of *ALTs, that might be excessive and we may want to revisit the policy. So go ahead and do this for now.

BTW both *OLD and *ALT should have "(Proof modification is discouraged.) (New usage is discouraged.)" in their comment. A *OLD should also have "Obsolete version of ~ xxx as of dd-mmm-yyyy." in the comment, not enclosed in parentheses.

In the comment for a *ALT, you might want to say (for xxxALT) "Has a shorter proof than ~ xxx but uses more axioms."

[david-a-wheeler]

I would just like to add that it is really really cool that OpenAI models are being used to simplify proofs. I think that artificial intelligence systems are very much going to be increasing in their capabilities in the world of proof, and this is another example of that. Thank you so much for this work.

I do agree that we'll have to be careful to not add axioms that were not depended on before, but that is something that can be addressed.

[spolu]

@david-a-wheeler thanks! looking forward to contributing more closely as we make progress 👍

[spolu]

@nmegill amended, rebased and ready to merge!

None of the shortened proofs introduce new ax-* axioms dependence. So I moved all current proofs as *OLD.

Most shortened proofs use less definitions. I believe only intss uses more definition in case you want to look into it more closely:

(base) ➜  set.mm git:(openai-shorten) ../metamath-exe/metamath 'read set.mm' 'show trace_back intssOLD /axioms' 'quit'

Metamath - Version 0.178 10-Aug-2019          Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 37500556 bytes
37500556 bytes were read into the source buffer.
The source has 176367 statements; 2503 are $a and 35095 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> show trace_back intssOLD /axioms
Statement "intssOLD" assumes the following axioms ($a statements):
  wn wi ax-mp ax-1 ax-2 ax-3 wb df-bi wa df-an wal cv wceq wtru df-tru wex
  df-ex wnf df-nf ax-gen ax-4 ax-5 wsb df-sb ax-6 ax-7 wcel ax-10 ax-11 ax-12
  ax-13 ax-ext cab df-clab df-cleq df-clel wnfc df-nfc cvv df-v cin wss df-in
  df-ss cint df-int
MM> quit
(base) ➜  set.mm git:(openai-shorten) ../metamath-exe/metamath 'read set.mm' 'show trace_back intss /axioms' 'quit' 

Metamath - Version 0.178 10-Aug-2019          Type HELP for help, EXIT to exit.
MM> read set.mm
Reading source file "set.mm"... 37500556 bytes
37500556 bytes were read into the source buffer.
The source has 176367 statements; 2503 are $a and 35095 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> show trace_back intss /axioms
Statement "intss" assumes the following axioms ($a statements):
  wn wi ax-mp ax-1 ax-2 ax-3 wb df-bi wo wa df-or df-an wal cv wceq wtru df-tru
  wex df-ex wnf df-nf ax-gen ax-4 ax-5 wsb df-sb ax-6 ax-7 wcel ax-10 ax-11
  ax-12 ax-13 ax-ext cab df-clab df-cleq df-clel wnfc df-nfc wral df-ral cin
  wss df-in df-ss cint df-int
MM> quit

[nmegill]

Great!

While using fewer definitions might be considered a tiny bit nicer, I'm not too concerned about it, and it isn't something we generally focus on or pay attention to. The command I usually use to determine axiom usage is "show trace_back intss /axioms/match ax-*". (The /axioms is unnecessary but suppresses a "($a)" suffix on the axioms.)

BTW the current metamath.exe version is 0.181 (12-Feb-2020), although the changes from your version shouldn't affect anything you are doing.

2nd BTW traditionally we have put the *OLD after the new version, and a long time ago this was done to help prevent the accidental usage of the *OLD to shorten the proof of the new one to one step thus erasing the proof shortening. This ceased to be a problem after the "(New usage is discouraged.)" tag was implemented. So I don't think it matters, except that people may be used to clicking the "Next" link on the web page to see the previous version of the proof. Anyone want to comment on this?

[spolu]

@nmegill thanks!

Submitted #1549 to reorder if that's what is the default usage in set.mm 👍

[david-a-wheeler]

@nmegill - I think it's best to continue to put the "OLD" proofs after the "main" proof, so that if you moving forward you see the "main proof for use" first.