Thanks for saying something.
I don't seem to have the ability to merge this one either. Perhaps we
can get some or all of the people who have write access to set.mm,
metamath-exe, etc to have write access here too. I don't know whether
merging the pull request is enough to get it on the web site, though, or
whether there is an additional step.
In happier news, I had not noticed until now that these files are now in
git. We knew that it would not be a small amount of work to get
everything in version control with working pull request and deploy
processes for everything. I'm sure we'd all like this to be going faster
or more smoothly, but I'm glad to see that there is a little progress,
even if there is plenty left to do.
On 12/11/22 02:21, Samiro Discher wrote:
As a remainder, none of my contributions have yet been merged. I
created a pull request
<https://github.com/metamath/metamath-website-seed/pull/1> to
@metamath/metamath-website-seed
<https://github.com/metamath/metamath-website-seed> as well. My
commits were accepted by Mario just minutes afterwards, but neither
were they merged, nor has Metamath's pmproof.txt
<https://us.metamath.org/mmsolitaire/pmproofs.txt> been updated by
now. A separate mail to David triggered no response.
Does nobody with access feel responsible for the mmsolitaire project?
— Samiro Discher
Samiro Discher schrieb am Donnerstag, 6. Oktober 2022 um 21:50:28 UTC+2:
I'd like to contribute my findings to
https://us.metamath.org/mmsolitaire/pmproofs.txt.
I found several (17) shorter proofs. See 'pmproofs.txt' at
https://github.com/xamidi/mmsolitaire [changes: 2be2349
<https://github.com/xamidi/mmsolitaire/commit/2be2349a5621eaaee5d5940e98202bd265c9d50a>]:
*2.62: 89 -> 77
*3.31: 103 -> 83
*3.43: 137 -> 117
*3.44: 203 -> 183
*4.14: 321 -> 283
*4.32: 355 -> 317
*4.39: 609 -> 479
*4.41: 271 -> 249
*4.76: 271 -> 249
*4.77: 375 -> 287
*4.86: 617 -> 557
*4.87: 523 -> 447
*5.31: 119 -> 109
*5.6: 203 -> 167
*5.75: 387 -> 351
meredith: 145 -> 141
biass: 2127 -> 1883
Furthermore, I modified another 26 proofs such that all subproofs
of the same formula (ranging over the whole collection) are equal
(preferring the lexicographically smaller proof strings). See
'pmproofs-unified.txt'. Feel free to use its contents if desired.
I find that property useful since this way, there are no redundant
proofs when parsing the collection, which saves time and space and
determines ideal and unique references. To showcase this, I
uploaded example files of the parsed collections to
https://github.com/xamidi/mmsolitaire/tree/master/data. The string
"pmproofs_/n/" in a filename indicates that helper proofs are
referenced for parts that are used in at least /n/ different proofs.
My findings were assisted by a custom tool I wrote in C++ (still a
private GitHub repo for assisting my research), and I have – If I
didn't mess something up – exhaustively searched all proofs up to
a length of 29 steps.
— Samiro Discher
PS: The contact information on the Metamath website and in
pmproofs.txt is still of Dr. Norman Megill. At first I tried to
use it despite him being deceased, and got no respone from anyone.
PPS: Is there a way I can add a non-Google mail address to this
mailing list?
--
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/60335b00-a53d-4716-a91a-0c959c1ad9a5n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/60335b00-a53d-4716-a91a-0c959c1ad9a5n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/fac9e3c0-9c2a-77ba-5663-abfb30e6dc17%40panix.com.
