Update: "?" and "$" are now used in the search tool instead of "." and ".*". (as suggested by Mario Carneiro)
Auguste Le mercredi 8 juillet 2020 à 23:49:28 UTC+2, [email protected] a écrit : > Great recommandation, thanks Mario. > > We’ll change that. > > -stan > > On Wed, Jul 8, 2020 at 8:46 PM Mario Carneiro <[email protected]> wrote: > >> A minor recommendation, but perhaps instead of "." and ".*", you could >> use "?" and "$", which matches the use in the metamath search command? >> (Technically "?" only matches one character tokens in metamath search but I >> think your version is more useful.) >> >> Mario >> >> On Wed, Jul 8, 2020 at 2:39 PM Auguste Poiroux < >> [email protected]> wrote: >> >>> Hi! >>> >>> Along with our proof assistant, we (OpenAI) are happy to share a simple >>> search tool for set.mm theorems, available without authentication at: >>> https://mmproofassistant.azurewebsites.net/search >>> >>> This tool offers two ways to search for theorems: by label, or by >>> hypotheses and conclusion. When searching for a theorem by hypotheses or >>> conclusion, you can use two RegExp-inspired wildcards: >>> - . : replaces any Metamath constant or variable (ex: Scalar, A, >>> i^i, ...). >>> - .* : replaces any sequence of space-separated Metamath variable or >>> constants. >>> >>> A few example searches that you may find useful:(i) "( ( . + . ) - . ) >>> = ( ( . - . ) + . )" returns addsub, addsubi and addsubd. >>> (ii) "mod .* = 0 <->" returns: >>> - mod0: |- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A / B ) >>> e. ZZ ) ) >>> - negmod0: |- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( -u A >>> mod B ) = 0 ) ) >>> - absmod0: |- ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( ( abs >>> ` A ) mod B ) = 0 ) ) >>> (iii) You can search by hypotheses (by adding search strings prefixed by >>> a yellow turnstile), "( . -> . )" and "." quickly finds ax-mp (despite the >>> different ordering of hypotheses). >>> (iv) Searching for syl3anc, "( . /\ . /\ . ) -> ." and "( ph -> . )" as >>> hypotheses and "( ph -> . )" as conclusion will work. >>> >>> We updated our tutorial with a new Section providing more details about >>> the search toool: >>> https://cdn.openai.com/openai_proof_assistant_tutorial.pdf >>> >>> We have been using this tool internally for a few weeks now and have >>> been enjoying it and hope it will help you find theorems more easily as >>> well! >>> >>> Auguste >>> >>> -- >>> 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/9410d276-cf80-498d-87bc-e88295a82839n%40googlegroups.com >>> >>> <https://groups.google.com/d/msgid/metamath/9410d276-cf80-498d-87bc-e88295a82839n%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/CAFXXJSs2AB0mmvS3aq9r6LiHFvvnNnqo5uA0_s1odgSUwXQhtg%40mail.gmail.com >> >> <https://groups.google.com/d/msgid/metamath/CAFXXJSs2AB0mmvS3aq9r6LiHFvvnNnqo5uA0_s1odgSUwXQhtg%40mail.gmail.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/56436970-bf5a-483f-8ae5-ee79d753aeffn%40googlegroups.com.
