Thank you so much for looking into this.

-stan

On Fri, Jul 10, 2020 at 9:25 PM 'Alexander van der Vekens' via Metamath <
[email protected]> wrote:

> 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
>
>
> --
> 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/c2970a38-da10-4185-a25d-c3f2c3b26a70o%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/c2970a38-da10-4185-a25d-c3f2c3b26a70o%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>

-- 
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/CACZd_0yW2ATqaoiy4xS3did_%3DQjTS%3DonAVBaL8eb_7hvWWYHiw%40mail.gmail.com.

Reply via email to