Il giorno venerdì 4 luglio 2025 alle 13:02:22 UTC+2 [email protected] ha
scritto:
Here is an example:
$(x^a)^b=x^{a\cdot b} \land a,b \in\mathbb{Q}$
or you can go with the vibe search approach and ask something "what's the
metamath set.mm theorem that looks like a^b^c = a^(b*c)"
DeepSeek returns ~ expmul
ChatGPT hallucinates a couple of nonexistent theorems, but it also returns
~ expmul as a "related theorem"
Of course, you can also go the boring way and use the search tools that you
can find in all proof assistants: metamath.exe, mmj2, and yamma.
metamath-lamp <https://expln.github.io/lamp/v29/index.html> is an online PA
(nothing to install) and it is probably the one with the most advanced
search features.
I would search for constant symbols. In your example, I would search for ^c
and x. and I'm pretty sure you'd find what you're looking for.
Note that ^ and ^c are distinct. For further details, refer to ~ cxpexp.
This distinction highlights the different domains of application for ~
cxpmul (as suggested by Mario) and ~ expmul (as suggested by DeepSeek).
--
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 visit
https://groups.google.com/d/msgid/metamath/bda670c7-235a-4c0d-8f88-c5ee290d1c5dn%40googlegroups.com.
