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/CACZd_0wWxcBXRFMv1zdAzE9RCOQe%2Buhf%2BOei6bba6Ek%3DDnQoRg%40mail.gmail.com.
