As a remainder, none of my contributions have yet been merged. I created a pull request <https://github.com/metamath/metamath-website-seed/pull/1> to @metamath/metamath-website-seed <https://github.com/metamath/metamath-website-seed> as well. My commits were accepted by Mario just minutes afterwards, but neither were they merged, nor has Metamath's pmproof.txt <https://us.metamath.org/mmsolitaire/pmproofs.txt> been updated by now. A separate mail to David triggered no response. Does nobody with access feel responsible for the mmsolitaire project?
— Samiro Discher Samiro Discher schrieb am Donnerstag, 6. Oktober 2022 um 21:50:28 UTC+2: > 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/60335b00-a53d-4716-a91a-0c959c1ad9a5n%40googlegroups.com.
