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.
