Awesome, very interesting. My concern is there are a lot of candidates in
the database which have this type of structure. You are quite correct re
brel, here is it's output:
⊢ ( A < B -> ( A e. RR* /\ B e. RR* ) )
0.91 brel
⊢ < C_ ( RR* X. RR* )
1.00 ltrelxr
If you are interested in the tool Stan talks about it here
<https://groups.google.com/d/msg/metamath/D09W2QVR-_I/g_rsqGj0AAAJ> and his
email is in the intro pdf
<https://cdn.openai.com/openai_proof_assistant_tutorial.pdf> if you want to
get credentials.
I'd recommend it, it's really interesting to play with and eventually it
will take over from humans in mathematics so it's worth trying to get on
it's good side while we have the chance :)
--
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/5698700c-2f17-47a7-ab2f-59b57091042bo%40googlegroups.com.
