Does anyone know an answer to my question > PPS: Is there a way I can add a non-Google mail address to this mailing list? I tried to send an email to metamath+subscribe at googlegroups dot com, but got a response "Your request to join metamath failed because you are already a member." which is not true (at least I receive nothing from this mailing list at that address and cannot find it in the list of members). Maybe some people have permission to invite arbitrary addresses into the list?
Also I noticed a mistake in my last comment: > Now for a proof that has m uses of a certain conclusion where that conclusion has n shortest (known) proofs, there is a number of m to the power of n ways It should say "n to the power of m". Something I still wanted to mention is that in one of the 17 cases (*5.75) I got lucky enough that its "result of proof" is a proper schema of the former one, which is visible here <https://github.com/xamidi/mmsolitaire/commit/2be2349a5621eaaee5d5940e98202bd265c9d50a#diff-fab5e13993fbe8ea945207911a5554433bf4b80770f3db4d22161fb5468ef5acL1373-L1376> . The nicely visible change (using the UI of my tool): [image: T5.75-improvement.png] In case anyone wants an overview / spoilers of what to expect from my tool, I made a public standalone <https://deontic-logic.github.io/readme.html> html file from my private repo's README.md. The mmsolitaire stuff is mentioned under "Introduction" at the fourth bullet point. Based on feedback, I might also extract some of the functionalities into a different but public repo since it can take a long time until certain stuff in my main repo is ready to be published. — Samiro Discher On Mon, Oct 10, 2022 at 1:19 AM Benoit <[email protected]> wrote: > Thanks Samiro. Yes, that's very readable and interesting. So, no > particular heuristic, but highly optimized exhaustive search of small > proofs, which then serve as building blocks for the longer ones. > > As for "ties" in shortest know proofs, you' re right, there are > exponentially many and it's probably not useful to keep multiple ones. > > Benoît > On Monday, October 10, 2022 at 12:37:39 AM UTC+2 [email protected] wrote: > >> Yeah, ideally we'd get all these files in git so we can use our regular >> process. But I don't want to too strongly push more work onto David and >> Mario (unless there is something I can do to help). >> >> On October 9, 2022 1:08:14 PM PDT, "David A. Wheeler" < >> [email protected]> wrote: >> >>> >>> >>> On Oct 9, 2022, at 3:05 PM, 'Samiro Discher' via Metamath >>> <[email protected]> wrote: >>>> I hope this is somewhat readable, if something is still unclear, feel free >>>> to ask. And let's hope at least David is still alive .. (´ ∀ ` *) >>>> >>> >>> Me too :-). >>> >>> Mario can certainly accept changes to it. Changes in the "seed" are rare, >>> but I think we should use the same process: someone proposes it, someone >>> else reviews & approves it, then it can be merged (accepted). >>> >>> --- David A. Wheeler >>> >>> -- >>> 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/7A642A67-E123-4824-B5E4-6DA398978F54%40dwheeler.com. >>> >>> -- > 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/3ee03c87-b202-4222-a28b-3146b5f176c2n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3ee03c87-b202-4222-a28b-3146b5f176c2n%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/CAJDHtD%3D8-ea%3DXHpn%3DF1v07LfMg%2BS8JekMUw3t3U_C-DnUzv47w%40mail.gmail.com.
