I'd like to contribute my findings to https://us.metamath.org/mmsolitaire/pmproofs.txt.
I found several (17) shorter proofs. See 'pmproofs.txt' at https://github.com/xamidi/mmsolitaire [changes: 2be2349 <https://github.com/xamidi/mmsolitaire/commit/2be2349a5621eaaee5d5940e98202bd265c9d50a> ]: *2.62: 89 -> 77 *3.31: 103 -> 83 *3.43: 137 -> 117 *3.44: 203 -> 183 *4.14: 321 -> 283 *4.32: 355 -> 317 *4.39: 609 -> 479 *4.41: 271 -> 249 *4.76: 271 -> 249 *4.77: 375 -> 287 *4.86: 617 -> 557 *4.87: 523 -> 447 *5.31: 119 -> 109 *5.6: 203 -> 167 *5.75: 387 -> 351 meredith: 145 -> 141 biass: 2127 -> 1883 Furthermore, I modified another 26 proofs such that all subproofs of the same formula (ranging over the whole collection) are equal (preferring the lexicographically smaller proof strings). See 'pmproofs-unified.txt'. Feel free to use its contents if desired. I find that property useful since this way, there are no redundant proofs when parsing the collection, which saves time and space and determines ideal and unique references. To showcase this, I uploaded example files of the parsed collections to https://github.com/xamidi/mmsolitaire/tree/master/data. The string "pmproofs_*n*" in a filename indicates that helper proofs are referenced for parts that are used in at least *n* different proofs. My findings were assisted by a custom tool I wrote in C++ (still a private GitHub repo for assisting my research), and I have – If I didn't mess something up – exhaustively searched all proofs up to a length of 29 steps. — Samiro Discher PS: The contact information on the Metamath website and in pmproofs.txt is still of Dr. Norman Megill. At first I tried to use it despite him being deceased, and got no respone from anyone. PPS: Is there a way I can add a non-Google mail address to this mailing list? -- 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/2d6b7dec-a789-45cc-83d0-bad05343c00cn%40googlegroups.com.
