Congratulations ! Since that page of the website is not on git, I think only David can add your proposals. I checked both using drule.c.
As for your second proposal, that happened because you found "ties" among shortest known proofs, is that it ? Maybe it's worth keeping them all ? I'm curious to see that C++ tool when you publicly release it. I don't know when the number of "21 steps" in pmproofs.txt for exhaustive search was written, but being able to reach 29 steps, given the exponential nature of the problem, seems impressive. And also for the non-exhaustive part, the heuristics you're using are probably interesting. Benoît On Thursday, October 6, 2022 at 9:50:28 PM UTC+2 Samiro Discher wrote: > 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/b66d0cea-878b-4a6a-a263-56562313fc97n%40googlegroups.com.
