I just found an even shorter proof for ra4:
---------Clip out the proof below this line to put it in the source file:
( wi wral r19.21 biimpi ) ABFCDGABCDGFABCDEHI $.
---------The proof of "ra4" (45 bytes) ends above this line.
whereas the one recently found by OpenAI is:
---------Clip out the proof below this line to put it in the source file:
( wnf wi wral r19.21t biimpd ax-mp ) ACFZABGCDHZABCDHGZGELMNABCDIJK $.
---------The proof of "ra4" (67 bytes) ends above this line.
I'm going to submit it in a new PR.
Benoît
--
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/f8ea2772-8048-42da-8467-d82e6e8c4547%40googlegroups.com.
