Another remark, when starting from all challenge proofs from w4, i.e. by adding the result of ./pmGenerator --unfold data/w4.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -o data/tmp2.txt -d to w4-dProofs-GG.txt before proof compression, there are further reductions w4: (A2: 13819↦4215, L1: 11989↦2385).
[email protected] schrieb am Donnerstag, 9. Januar 2025 um 06:14:09 UTC+1: > > Hopefully everything is right. Fingers crossed. > > So it seems! As far as I can see, it reduces to 2437 steps towards L1 > using --transform -z, but I only used the five theorems from w4.mm (which > are ax1, id, luk1, luk2, th0), not the inferences — but you could still > use their greatest subproofs of theorems as well. I attached my translation > of your entire w4.mm to this mail (with inferences commented out). > > $ ./pmGenerator -c -n -s CpCCNqCCNrsCtqCCrtCrq --parse > data/w4-dProofs-GG.txt -f -n -s -d -o data/tmp.txt --transform data/tmp.txt > -f -n -t CCNpCCNqrCspCCqsCqp,CpCqp,Cpp,CCNppp,CCpqCCqrCpr -p -2 -d > > There are 3 steps towards CCNpCCNqrCspCCqsCqp / CCN0CCN1.2C3.0CC1.3C1.0 > (index 0). > > There are 59 steps towards CpCqp / C0C1.0 (index 13). > > There are 465 steps towards Cpp / C0.0 (index 21). > > There are 1703 steps towards CCNppp / CCN0.0.0 (index 22). > > There are 9513 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 23). > Using -z in the end resulted in: > > There are 3 steps towards CCNpCCNqrCspCCqsCqp / CCN0CCN1.2C3.0CC1.3C1.0 > (index 0). > > There are 59 steps towards CpCqp / C0C1.0 (index 13). > > There are 465 steps towards Cpp / C0.0 (index 21). > > There are 1703 steps towards CCNppp / CCN0.0.0 (index 22). > > There are 2437 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 23). > > Spoiler: My incoming w4:L1 will still be multiple times smaller (currently > 827, unphased by compressing with your proofs of theorems :-), and even > w4:id went down to 361 steps. > > > ------------------------------ > *Von:* [email protected] <[email protected]> im Auftrag von > Gino Giotto <[email protected]> > *Gesendet:* Mittwoch, 8. Januar 2025 22:40 > *An:* Metamath > *Betreff:* [Metamath] Re: Upcoming contributions to proof minimization > challenges > > I might have something. I created a Metamath database for Walsh's fourth > axiom https://github.com/GinoGiotto/w4.mm and my proof for luk1 seems > shorter than the current one. > > Preliminary information: > > - All theorems are complete and verified with metamath.exe. > > - I saved all proofs in the normal format because the compressed one shows > a lower step count (yes, this makes the database very big). > > - The command "SHOW TRACE_BACK luk1 /COUNT /ESSENTIAL" says that "The > proof would have 9513 steps if fully expanded back to > axiom references." which is lower than the 11989 step count in the table. > > So, if the metamath.exe count is correct and if I have not made rookie > mistakes then I have a shortening of luk1 in w4. I am not 100% confident > that everything is fine until I translate it into condensed detachment and > verify it with pmGenerator. > > This email is just to claim my (potential) result before the new proofs > arrive. I'm probably going to do the translation tomorrow or the day after > tomorrow, and I will also attempt to shorten the proof further with the > automatic compression algorithm. Hopefully everything is right. Fingers > crossed. > > > Il giorno lunedì 6 gennaio 2025 alle 12:44:29 UTC+1 > [email protected] ha scritto: > >> In probably at most a few weeks, I will post some weighty proof >> minimizations. >> I don't know if anyone else is currently working on those, but in this >> case I would suggest to hurry up. :-) >> >> >> - In Metamath's pmproofs.txt challenge >> <https://us.metamath.org/mmsolitaire/pmproofs.txt>, I am reducing at >> least *38 proofs* by at least * 1420 steps* total. >> >> >> - In my minimal 1-base challenge >> <https://github.com/xamidi/pmGenerator/discussions/2>, I am reducing >> at least *22 proofs* by at least *99312 steps* total. >> >> >> I am throwing a lot of computing power at a new proof compression >> <https://github.com/xamidi/pmGenerator/discussions/3> algorithm that I >> will release as part of pmGenerator >> <https://github.com/xamidi/pmGenerator> along with these contributions. >> >> Afterwards, it will be *extremely difficult* to make further non-tiny >> contributions (unless I missed something significant). >> >> >> — 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 visit > https://groups.google.com/d/msgid/metamath/a327629a-f1e2-4437-a6d9-50ae7095235an%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/a327629a-f1e2-4437-a6d9-50ae7095235an%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/8a23f768-94fa-4ac7-ad35-0c5737b158afn%40googlegroups.com.
