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.
