I think in the long term we might want to treat 'pmproof.txt' as a proper database; involving proof verification, markup verification, and essentially the important features already implemented for the main ones. It seems there is enough interest for this project, but Metamath users might not even know that it exists as it is somewhat hidden both on the webpage and on Github. For example, in 2023 an user attempted <https://github.com/metamath/set.mm/pull/3622>to submit a shorter proof back to the axioms in set.mm, but the revision was not accepted because it was longer in the compressed format. I think this confusion can be avoided by integrating the pmproof.txt database into the set.mm repository (perhaps into a Metamath Solitaire folder?), and add it to the table of databases at the beginning of the Metamath front page (although a Metamath Solitaire explorer might need to avoid showing the proof formulas, as they tend to be very long). Il giorno domenica 16 giugno 2024 alle 03:53:59 UTC+2 [email protected] ha scritto:
> I have found an additional 40 shorter proofs for > https://us.metamath.org/mmsolitaire/pmproofs.txt. See 'pmproofs.txt' at > https://github.com/xamidi/mmsolitaire [changes: f9a40e7 > <https://github.com/xamidi/mmsolitaire/commit/f9a40e79bf8764c11b1b891eae58c2fdbce15293> > ]: > *2.32: 91 -> 83 > *3.3: 59 -> 55 > *3.33: 95 -> 73 > *3.34: 105 -> 73 > *3.43: 117 -> 109 > *3.44: 181 -> 161 > *3.47: 203 -> 199 > *3.48: 241 -> 171 > *4.14: 283 -> 263 > *4.15: 277 -> 233 > *4.32: 317 -> 313 > *4.33: 207 -> 199 > *4.38: 585 -> 529 > *4.39: 479 -> 465 > *4.4: 355 -> 345 > *4.41: 249 -> 241 > *4.52: 219 -> 209 > *4.53: 169 -> 159 > *4.72: 195 -> 193 > *4.76: 249 -> 241 > *4.77: 285 -> 265 > *4.82: 175 -> 157 > *4.83: 245 -> 231 > *4.85: 121 -> 119 > *4.86: 555 -> 551 > *4.87: 447 -> 439 > *5.15: 267 -> 185 > *5.16: 333 -> 331 > *5.18: 503 -> 491 > *5.23: 513 -> 501 > *5.33: 389 -> 343 > *5.35: 159 -> 145 > *5.53: 673 -> 633 > *5.54: 239 -> 233 > *5.6: 167 -> 163 > *5.61: 259 -> 249 > *5.62: 167 -> 157 > *5.74: 337 -> 335 > *5.75: 351 -> 331 > biass: 1877 -> 1851 > > For this, I used a new "proof compression" feature (parameter '-z' for > '--transform') of pmGenerator <https://github.com/xamidi/pmGenerator> (to > be released in version 1.2.1), > which was mainly inspired by Gino Giotto from this comment > <https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-9769069> > > and his corresponding solution. > > While Gino (to my surprise) found an argument that could be replaced by an > axiom (technically, by any theorem), > only 1 out of 69 elementary improvements for pmproofs.txt was of that > nature, all others were replacements of one or both inputs of a D-rule with > proofs of non-trivial theorems. > > Indeed, the feature does not only test for axioms but for all formulas > that occur in a proof summary, and tries all combinations of such formulas > as arguments of a D-rule, as long as the overall result would be shorter > than before. > > The compression took roughly five and a half hours and was based on > 'pmproofs-summary.txt', which I shared a few months ago on this mailing > list <https://groups.google.com/g/metamath/c/eHW5779KfXU/m/A2WAkOamAQAJ>. > (It usually takes only a few seconds to minutes for proof summaries of > reasonable size, but pmproofs' collection is rather large.) > More details — which commands I used and what output they gave — can be > seen in the appendix ('pm-z-improvements.log'). > > The new feature also led to quite a few more improvements > <https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-9784395> > > of the minimal C-N 1-base challenge. > > Thanks to Gino for the inspiring and motivating comments. :-) > > > — Samiro Discher > > -- 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/6029d44d-d5a3-4692-b992-f4754a312629n%40googlegroups.com.
