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.
