OpenAI search tool for set.mm theorems

[Auguste Poiroux]

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

[Mario Carneiro]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9410d276-cf80-498d-87bc-e88295a82839n%40googlegroups.com.

[Stanislas Polu]

Great recommandation, thanks Mario.

We’ll change that.

-stan

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSs2AB0mmvS3aq9r6LiHFvvnNnqo5uA0_s1odgSUwXQhtg%40mail.gmail.com.

[Auguste Poiroux]

Update: "?" and "$" are now used in the search tool instead of "." and ".*".  (as suggested by Mario Carneiro)

Auguste