As previously announced <https://groups.google.com/g/metamath/c/xM3FmOwtxvg/m/BlPbmKxsBwAJ>, I created some big improvements for our proof minimization challenges. These are my final results:
- In Metamath's pmproofs.txt <https://us.metamath.org/mmsolitaire/pmproofs.txt> challenge, I reduced *38 proofs* by *1430 steps* total <https://github.com/xamidi/mmsolitaire/commit/9bb17b0553ad92d7d40aa6efb57bde668c2e62f9>. [pull request <https://github.com/metamath/metamath-website-seed/pull/29>] - Files to document the solution procedure and progression: pmMinimization.7z <https://github.com/user-attachments/files/18978973/pmMinimization.7z.zip> (3'260'031 bytes compressed into 216'203 bytes) I also included all proofs of past versions of pmproofs.txt (when available on the Wayback Machine or on metamath.org), but appending them to proof compression resulted in no further improvements towards target theorems. However, these past pmproofs.txt versions are available in 'pmMinimization.7z/data/pmproofs-versions.7z'. - In the minimal 1-base challenge, I reduced *23 proofs* to a total of *22561 steps left* <https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-12323006> . Regarding proofs in minimal 1-bases, I reached a major milestone by falling below 25000 proof steps combined. This is quite significant, given that when I started this challenge in March last year, the best I could do was three proofs unknown with the remaining proofs having 3'207'984 steps in total <https://github.com/xamidi/pmGenerator/discussions/2#hall-of-fame>. My corresponding post is meant to provide insights on how pmGenerator's new proof compression feature can be used, and how it currently performs. Got any questions? Please ask here or in the discussions forum <https://github.com/xamidi/pmGenerator/discussions>! List of new improvements in pmproofs.txt: *2.73: 165 -> 153 ( -12) *2.82: 91 -> 89 ( -2) *3.48: 171 -> 167 ( -4) *4.11: 363 -> 359 ( -4) *4.12: 363 -> 359 ( -4) *4.15: 233 -> 205 ( -28) *4.22: 273 -> 271 ( -2) *4.36: 271 -> 219 ( -52) *4.37: 307 -> 255 ( -52) *4.38: 529 -> 527 ( -2) *4.39: 465 -> 463 ( -2) *4.42: 165 -> 157 ( -8) *4.52: 209 -> 207 ( -2) *4.53: 159 -> 157 ( -2) *4.78: 319 -> 191 (-128) *4.79: 383 -> 259 (-124) *4.83: 231 -> 197 ( -34) *4.86: 551 -> 473 ( -78) *5.1: 107 -> 87 ( -20) *5.15: 185 -> 161 ( -24) *5.17: 329 -> 285 ( -44) *5.19: 123 -> 105 ( -18) *5.21: 115 -> 111 ( -4) *5.22: 363 -> 333 ( -30) *5.24: 585 -> 545 ( -40) *5.3: 127 -> 125 ( -2) *5.31: 109 -> 105 ( -4) *5.32: 625 -> 621 ( -4) *5.33: 343 -> 311 ( -32) *5.35: 145 -> 129 ( -16) *5.36: 381 -> 257 (-124) *5.53: 633 -> 551 ( -82) *5.54: 233 -> 149 ( -84) *5.55: 167 -> 165 ( -2) *5.61: 249 -> 231 ( -18) *5.7: 673 -> 605 ( -68) *5.74: 335 -> 333 ( -2) biass: 1851 -> 1579 (-272) -- 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 visit https://groups.google.com/d/msgid/metamath/f8d5e416-59b7-4c38-a4dd-d8d361746ffan%40googlegroups.com.
