I could reduce five more proofs [changes: 21911f8 <https://github.com/xamidi/mmsolitaire/commit/21911f8de1de822697d4576f800f97afcb61d7b9> ]: *3.44: 183 -> 181 *4.77: 287 -> 285 *4.85: 123 -> 121 *4.86: 557 -> 555 biass: 1883 -> 1877
28 more proofs are affected by unification to lexicographically smallest known proof (sub-)strings. I created a corresponding pull request <https://github.com/metamath/metamath-website-seed/pull/4>. Correctness of the resulting collection can be automatically verified, for example, via pmGenerator -a SD data/empty.txt data/pmproofs.txt data/pmproofs-unwrapped.txt -s -l -d which parses and reassembles the database at ./data/pmproofs.txt, given an empty file at ./data/empty.txt. Parse errors are printed for invalid proofs. All 5 shortenings occurred thanks to finding DD2D12DD2D13DD2D1DD22D11DD2D11DD2D131 (length 37) as a minimal proof for CNC0NC1.2CC3.1C3.2 [i.e. ~ (P -> ~ (Q -> R)) -> ((S -> Q) -> (S -> R))], for which previously DD2D1DD2D121D3DD2D1D3DD2DD2D13DD2D13111 (length 39) was used, which occurred once in each of *3.44, *4.77, *4.85, *4.86, and three times in biass. I used pmGenerator <https://github.com/xamidi/pmGenerator> for computation of the discovery. Generation and utilization of dProofs37-unfiltered31+.txt were performed with computing resources granted by RWTH Aachen University under project rwth1392. A CLAIX-2016 SMP node with 1024 GB main memory was sufficient to load the amount of data, whereas CLAIX-2018 does not have nodes with sufficient amounts of memory. The latest proof file (dProofs37-unfiltered31+.txt) alone contains 506656999 proofs and conclusions, which make 113174356461 bytes (approx. 105.40 GiB) in data. Since generating the next file (dProofs39-unfiltered31+.txt) is impossible on CLAIX-2016 SMP nodes within granted time frames (7 days maximum duration of production job runs) and memory, next I will not go further down the *-unfiltered31+ line, but instead I am looking into MPI-based filtering, possibly allowing for smaller databases (e.g. ..., dProofs31.txt, dProofs33-unfiltered33+.txt, ...). Filtering existing databases is distributed memory friendly, in contrast to the generation of increasing databases (as previously mentioned <https://groups.google.com/g/metamath/c/6DzIY33mthE/m/K0I6UNoiAgAJ>). Very friendly, in fact: The number of distributed computing nodes for which the job duration shrinks, is in theory only limited by O(cardinality of the shrinkable set of proofs). For example, to shrink dProofs31-unfiltered31+.txt (which contains 13194193 proofs) to dProofs31.txt, one could use up to 13194193 nodes to shrink the required time frame (when each redundancy check is not further distributed). Such an extensive parallelization would probably require entire nodes dedicated to data acquisition, but — for practical purposes — I will only have the main node acquire data while also checking for redundancy of its own subset of proofs. The results should be reproducible via commands 1. pmGenerator -g 29 2. pmGenerator -g 37 -u 3. pmGenerator -r data/pmproofs.txt data/pmproofs-reducer37.txt -d 4. pmGenerator -a SD data/pmproofs-reducer37.txt data/pmproofs.txt data/pmproofs-result37.txt -s -l -w -d on a machine with sufficient resources, and the relative path ./data/pmproofs.txt referencing pmproofs.txt <https://us.metamath.org/mmsolitaire/pmproofs.txt> of version 03-Oct-2022. Assuming correctness of the implementation, all proofs up to a length of 37 steps were exhaustively searched. — 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 on the web visit https://groups.google.com/d/msgid/metamath/32c478fe-51e6-415f-b614-04a9354de14bn%40googlegroups.com.
