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/36e82da9-b718-4543-8976-cc24957be11en%40googlegroups.com.
