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.
