Thank you so much for looking into this.
-stan
On Fri, Jul 10, 2020 at 9:25 PM 'Alexander van der Vekens' via Metamath <
metamath@googlegroups.com> wrote:
> Hi Stan,
> with PR #1715, the proofs of the following theorems are replaced by the
> proofs shortened by OpenAI for the following theorems
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
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
On Tue, Jul 7, 2020 at 5:46 PM Norman Megill wrote:
>
> This is nice work Stanislas, thank you.
>
> On Friday, July 3,
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
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
On Mon, Jul 6, 2020 at 12:40 PM 'Alexander van der Vekens' via
Metamath
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
