Another contribution to Metamath's mmsolitaire project

[samiro.d...@rwth-aachen.de]

I have found an additional 40 shorter proofs for https://us.metamath.org/mmsolitaire/pmproofs.txt. See 'pmproofs.txt' at https://github.com/xamidi/mmsolitaire [changes: f9a40e7]:
*2.32:    91 ->   83
*3.3:     59 ->   55
*3.33:    95 ->   73
*3.34:   105 ->   73
*3.43:   117 ->  109
*3.44:   181 ->  161
*3.47:   203 ->  199
*3.48:   241 ->  171
*4.14:   283 ->  263
*4.15:   277 ->  233
*4.32:   317 ->  313
*4.33:   207 ->  199
*4.38:   585 ->  529
*4.39:   479 ->  465
*4.4:    355 ->  345
*4.41:   249 ->  241
*4.52:   219 ->  209
*4.53:   169 ->  159
*4.72:   195 ->  193
*4.76:   249 ->  241
*4.77:   285 ->  265
*4.82:   175 ->  157
*4.83:   245 ->  231
*4.85:   121 ->  119
*4.86:   555 ->  551
*4.87:   447 ->  439
*5.15:   267 ->  185
*5.16:   333 ->  331
*5.18:   503 ->  491
*5.23:   513 ->  501
*5.33:   389 ->  343
*5.35:   159 ->  145
*5.53:   673 ->  633
*5.54:   239 ->  233
*5.6:    167 ->  163
*5.61:   259 ->  249
*5.62:   167 ->  157
*5.74:   337 ->  335
*5.75:   351 ->  331
biass:  1877 -> 1851

For this, I used a new "proof compression" feature (parameter '-z' for '--transform') of pmGenerator (to be released in version 1.2.1),
which was mainly inspired by Gino Giotto from this comment and his corresponding solution.

While Gino (to my surprise) found an argument that could be replaced by an axiom (technically, by any theorem),
only 1 out of 69 elementary improvements for pmproofs.txt was of that nature, all others were replacements of one or both inputs of a D-rule with proofs of non-trivial theorems.

Indeed, the feature does not only test for axioms but for all formulas that occur in a proof summary, and tries all combinations of such formulas as arguments of a D-rule, as long as the overall result would be shorter than before.

The compression took roughly five and a half hours and was based on 'pmproofs-summary.txt', which I shared a few months ago on this mailing list. (It usually takes only a few seconds to minutes for proof summaries of reasonable size, but pmproofs' collection is rather large.)
More details — which commands I used and what output they gave — can be seen in the appendix ('pm-z-improvements.log').

The new feature also led to quite a few more improvements of the minimal C-N 1-base challenge.

Thanks to Gino for the inspiring and motivating comments. :-)

— Samiro Discher

[Gino Giotto]

I think in the long term we might want to treat 'pmproof.txt' as a proper database; involving proof verification, markup verification, and essentially the important features already implemented for the main ones. It seems there is enough interest for this project, but Metamath users might not even know that it exists as it is somewhat hidden both on the webpage and on Github. For example, in 2023 an user attempted to submit a shorter proof back to the axioms in set.mm, but the revision was not accepted because it was longer in the compressed format. I think this confusion can be avoided by integrating the pmproof.txt database into the set.mm repository (perhaps into a Metamath Solitaire folder?), and add it to the table of databases at the beginning of the Metamath front page (although a Metamath Solitaire explorer might need to avoid showing the proof formulas, as they tend to be very long).

[Mario Carneiro]

While I agree, this is a nontrivial task because pmproofs.txt is not a metamath database at all, it's a completely unrelated format which needs bespoke tools to process it. But I agree that we should have verification that the proofs in the file are actually correct, and while we're at it we may as well also ensure they have the claimed length.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6029d44d-d5a3-4692-b992-f4754a312629n%40googlegroups.com.

[samiro.d...@rwth-aachen.de]

> in the long term we might want [...] proof verification

> we should have verification that the proofs in the file are actually correct, and while we're at it we may as well also ensure they have the claimed length

The initial purpose of pmGenerator (before it even had that name) was to convert all proofs in pmproofs.txt into formula-based proofs, and validate them along the way.

So, whenever a proof database is parsed, this comes with automated validation, and when reassembled, its proof steps are counted automatically and printed into the output file.

Thus an easy way to verify both correctness and lengths is to reassemble pmproofs.txt via '-a' without applying any replacements (i.e. referring to an empty replacements file), like

$ ./pmGenerator -a XY empty.txt pmproofs.txt pmproofs-reassembled.txt -l -d -w

and then comparing 'pmproofs.txt' with  'pmproofs-reassembled.txt' to compare specified proof lengths.

The program should throw an error when any proofs are incorrect (if not, that'd be an issue), and otherwise the user can subsequently check whether the result is the same as in the original file, excluding the header.

For example, by pasting the contents of both files to a site such as https://www.textcompare.org/.

All file versions provided by me are verified by the tool, due to how they were processed and generated.

Exemplary output:

$ ./pmGenerator -a XY data/empty.txt data/pmproofs.txt data/pmproofs-reassembled.txt -l -d -w
Sun Jun 16 22:00:03 2024: Process started. [pid: 48532, tid:1]
Tasks:
1. applyReplacements("XY", "data/empty.txt", "data/pmproofs.txt", "data/pmproofs-reassembled.txt", false, true, true, true)

[Main] Calling applyReplacements("XY", "data/empty.txt", "data/pmproofs.txt", "data/pmproofs-reassembled.txt", false, true, true, true).
0.27 ms taken to read 0 shortening replacements and 0 styling replacements.
1.14 ms taken to read 196 condensed detachment proofs from file "data/pmproofs.txt".
0.00 ms taken to store 196 lengths.
0.03 ms taken to apply replacements.
202.27 ms taken to check, generate and save 54594 bytes of MM-styled condensed detachment proofs (0 shortened, 0 styled, 196 unmodified) to data/pmproofs-reassembled.txt.
Sun Jun 16 22:00:03 2024: Process terminated. [pid: 48532, tid:1]

Note: Omitting the '-w' will remove all line wrappings, which can make the individual D-proofs easier to use.

PS: Isn't drule.c (mentioned in the file's header) also able to validate all proofs in the file at once? I mean, it should, but maybe it just ignores some issues that can be ignored, like incorrectly lining up multiple correct D-proofs..

[Mario Carneiro]

I probably can't help that much, but I would encourage you to structure that as a CI script and make a PR to set.mm to run it in CI.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/22617d1f-2d29-4698-b090-720ad1529909n%40googlegroups.com.