Groups keyboard shortcuts have been updated
Dismiss
See shortcuts
Massive improvements found for pmproofs.txt and 1-base challenge
101 views
Skip to first unread message
samiro.d...@rwth-aachen.de
Feb 26, 2025, 5:57:36 AMFeb 26
to Metamath
As previously announced, I created some big improvements for our proof minimization challenges.
These are my final results:
- In Metamath's pmproofs.txt challenge, I reduced 38 proofs by 1430 steps total. [pull request]
- Files to document the solution procedure and progression: pmMinimization.7z (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.
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.
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!
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)
These are my final results:
- In Metamath's pmproofs.txt challenge, I reduced 38 proofs by 1430 steps total. [pull request]
- Files to document the solution procedure and progression: pmMinimization.7z (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.
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.
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!
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)
David A. Wheeler
Feb 26, 2025, 10:32:59 AMFeb 26
to Metamath Mailing List
> On Feb 26, 2025, at 5:57 AM, samiro.d...@rwth-aachen.de <samiro....@rwth-aachen.de> wrote:
>
> As previously announced, I created some big improvements for our proof minimization challenges.
--- David A. Wheeler
samiro.d...@rwth-aachen.de
Mar 20, 2025, 1:14:00 PMMar 20
to Metamath
Insofar there are no objections, could someone with permissions merge the pull request?
Jim Kingdon
Mar 20, 2025, 7:24:30 PMMar 20
to meta...@googlegroups.com
Merged.
If someone who knows more about pmproofs.txt than I do has
anything to say, speak up. But this seems like an improvement, so
I went ahead and merged it.
--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/285ea5ac-15e0-491b-8a98-5736d9f1108dn%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages