Dear Metamath community,
as part of celebrating the 2-year anniversary of the “Minimal 1-bases for C-N propositional calculus <https://github.com/xamidi/pmGenerator/discussions/2>” proof minimization challenge (PMC), today I am opening another PMC: “Traversing minimal classical C-N single axioms <https://github.com/xamidi/pmGenerator/discussions/10>”. Both are inspired from Metamath's PMC “Shortest known proofs of the propositional calculus theorems from *Principia Mathematica* <https://us.metamath.org/mmsolitaire/pmproofs.txt>” (aka 'pmproofs.txt'). The challenge mentioned first is about finding smaller effective/constructive proofs (i.e. derivations within the actual Hilbert system) from minimal 1-bases (i.e. down to a minimal single axiom with the detachment rule) for classical propositional logic that demonstrate their completeness. This is done by deriving the axioms of two systems of Polish logician Jan Łukasiewicz [who used *Polish notation* (PN) to present formulas]: (A1) ψ→(φ→ψ) [PN: CpCqp] (A2) (ψ→(φ→χ))→((ψ→φ)→(ψ→χ)) [PN: CCpCqrCCpqCpr] (A3) (¬ψ→¬φ)→(φ→ψ) [PN: CCNpNqCqp] (L1) (ψ→φ)→((φ→χ)→(ψ→χ)) [PN: CCpqCCqrCpr] (L2) (¬ψ→ψ)→ψ [PN: CCNppp] (L3) ψ→(¬ψ→φ) [PN: CpCNpq] I also included the smallest C-N tautology, (id) ψ→ψ [PN: Cpp], as a target theorem. Notably, (A1)–(A3) are also the propositional axioms of Metamath's “set.mm” database. Thanks also to valuable contributions from the Metamath community, specifically Gino Giotto and Steven Nguyen, we found the first constructive completeness proof for one of the seven minimal single axioms (w2: Walsh's 2nd axiom) on July 12, 2024. This solved an open challenge problem that was established by Walsh and Fitelson on June 26, 2021 — they had found constructive proofs for all but this axiom, which proved quite difficult to handle due to the generation of almost exclusively long formulas for very short proofs — see also this list of 1000 shortest theorems for w2-proofs of up to 43 steps <https://xamidi.github.io/pmGenerator/data/db25c49b13fec26ecf32e40bde65e4e2273f23b3c022cfd0fa986cff/top1000SmallestConclusions_1to43Steps.txt>. However, we have since found proofs from w2 that are much smaller than their counterparts in other 1-bases, which makes sense since the exhaustion barrier of w2 is the lowest of them all, i.e. the number of theorems explodes the fastest for longer proofs. In case you want to look at - the status of the 1-basis completeness PMC: https://github.com/xamidi/pmGenerator/discussions/2#challenge-proofs - the progression of the 1-basis completeness PMC: https://github.com/xamidi/pmGenerator/discussions/2#progress In my opinion, we made amazing progress. Not only in the scope of the challenge, since it also led to the discovery of very effective proof compression algorithms and the aforementioned resolution of the open challenge problem. *The new challenge* The new PMC is about deriving the minimal single axioms from one another in fewer amounts of steps than previously achieved. These proofs tend to be longer since larger theorems tend to have longer proofs. The shortest proofs I've found while preparing the new challenge <https://github.com/xamidi/pmGenerator/discussions/10#discussioncomment-15995488> mostly have step numbers in the 1000s rather than in the 10s and 100s, with not a single one known to be minimal (i.e. contained in an exhaustively generated set). These preparations, consisting of extensive computations over a period of nine months, also led to further improvements to the preceding challenge <https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-15995408> — from 22561 down to 18547 proof steps in total — along with the birth of a new preoptimized challenge. ;-) In contrast to 18547 total proof steps for 49 proofs (33 of which are not known to be minimial), the starting point for the new PMC is at 102278 total proof steps for 42 proofs. In case you want to look at - the status of the 1-basis traversal PMC: https://github.com/xamidi/pmGenerator/discussions/10#challenge-proofs - the progression of the 1-basis traversal PMC: https://github.com/xamidi/pmGenerator/discussions/10#progress I wish all participants the best of luck and lots of fun! Keep in mind, however, that these are some of the hardest challenges humanity has to offer, or as it was put regarding the mmsolitaire project <https://us.metamath.org/mmsolitaire/mms.html> by Dr. Norman D. Megill, founder of Metamath: You can play around with it for curiosity or fun, or if you're serious it will be the hardest "game" in the world! — Samiro Discher PS: This shouldn't even have to be mentioned but these challenges, and by extension the entire *pmGenerator* project, are no place for LLM-generated contents and contributions. To be clear, I never used them for anything related except testing whether they can get anything right and the clear answer is, no, they fail miserably at pretty much everything related to formal condensed detachment proofs, yet confidently claim the opposite and lie all the time! I don't even let LLMs assist me with coding because I think they're terrible garbage producing compulsive liars and deceivers, and producing bug-free high-quality code is much more important to me than getting things done faster with less effort. Nonetheless, I was already accused by some self-proclaimed "math nerd" on Reddit of producing AI slop after sharing my new introduction <https://github.com/xamidi/pmGenerator?tab=readme-ov-file#readme> (which took me several days to put together), where someone was apparently not understanding what they were reading. I hope this is clear enough to any reasonably educated person, and I am welcoming feedback. PPS: I documented all procedures of how I obtained the initial proofs for the new challenge with my *pmGenerator* tool within a file archive to reproduce these results. It is important to note that the used compression algorithms are inherently nondeterministic (due to parallelization), so using them from scratch might produce different results. But the vault files contain the exact findings and can be used to reconstruct the same proof collections. However, several of the procedures do not work with the (latest) 1.2.2 released binaries, but require more recent features. There will likely soon be the (sufficient) 1.2.3 release. This poses no issue if you build the executable from C++ on your own, which is required for non-Windows platforms regardless. -- 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/ecfef151-8115-452f-b102-97aa922ac83bn%40googlegroups.com.
