Finding the proof I need quickly and efficiently

[Alessandro Griseta]

As a future university student who has just finished High School, it's very easy for me to randomly have some doubt about a proof.

As a consequence I believe metamath has the incredible potential to allow anyone learning mathematics to fill gaps in their own knowledge and making the proof-memorising process (= basis of mathematics!) much more precise and methodical. Therefore the organisation has an excellent potential to become a valuable OER (Open Educational Resource).

Having said that, it's often quite hard to find the 'right' proof in the giant database metamath provides (`mmset`).

Here is an example:

$(x^a)^b=x^{a\cdot b} \land a,b \in\mathbb{Q}$

^^^ it isn't very formally explained here, but basically I'm looking for the proof that the power of a power is equal to the multiplication of powers, even when the powers are rational numbers. 

Any suggestions for pin-pointing the exact proof? I'd love to use and contribute to this database, but sadly, a bit like in real life, if I own something but I've lost it, it's like not owning it at all!

I'd also be happy to test out similar tools/resources. Otherwise, if you think I need some preliminary knowledge, please feel free to post links! Perhaps my problem is that I don't understand in which 'topics' metamath is grouped in, although I'm so new to metamath and its innovative approach that I'd appreciate some guidance first!

Thank you very much for your patience, I'll look forward to any kind of reply!

Alessandro

[Mario Carneiro]

The theorem you are looking for is https://us.metamath.org/mpeuni/cxpmul.html . Note that the assumptions are a bit different from what you have assumed: the complex power function works in general for arbitrary complex numbers rather than rational numbers, but because of various issues around branch cuts these kinds of theorems usually don't hold over the whole domain. This particular theorem, x^(ab) = (x^a)^b, is true as long as x is a positive real number and a,b are real numbers. (The formal theorem allows b to be complex, but not a.)

--
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 visit https://groups.google.com/d/msgid/metamath/1252faeb-9c6a-4932-bff9-8f9f3c679016n%40googlegroups.com.

[Meta Kunt]

Welcome Alessandro,

Metamath, and other computer assisted theorem provers, are designed for proving theorems in a very rigorous way.
Metamath in particular is a very small system that explains every proof step. So if there is a theorem in the database, you will be able to find a proof and browse it to your heart's content.

"I'd love to use and contribute to this database, but sadly, a bit like in real life, if I own something but I've lost it, it's like not owning it at all!"

Currently I don't know how to interpret this statement. Let me try to give you a different statement. To own something, you have to find/buy/obtain it first.
The thing that everyone here already obtained through a combination of either a higher mathematics education and/or working with metamath is knowledge.

Here is a non-exhaustive list of what I would focus on learning first:
Try to understand how informal mathematical proofs in prosa work. Learn how the induction principle works, learn the rules of propositional logic, learn how the quantors work.

Learn what sets are, what functions are, what images/pre-images are.
Learn how the real numbers are constructed. Well this is all basically in your first year math's curriculum, so take a good Analysis 1 book and familiarise yourself with it,

Metamath proofs are very verbose, every step has to be explained and every proof usually just has a few key ideas that make it work.
If I gave you a theorem in the database, you could browse the proof. But would you understand what it says? Would you know what the key ideas are?
Those are much better explained in prosa, but the technical details are often left out. You'll likely not see the forest for the trees.

If you still want to contribute, then the hard part and work begins. Everything that you've learned you can throw it out of the window.
Metamath is an extremely harsh and unforgiving system and at the beginning you will struggle with nearly every statement.
When I started, I already had obtained all the informal mathematical knowledge through a math's degree.
I still had to learn everything from zero, the only difference is I could understand the concepts and ideas quicker.
For you, it will likely be even harder and the learning curve will be even steeper.

Over time you'll what the patterns to use and what patterns to avoid. The database is mostly filled with useless theorems for your current proof. Finding stuff will indeed become a challenge.
But, if you see it as a video game, you'll start with level 1 and your first boss is already a level 50 elephant.
To defeat this elephant you will need to use a vast array of concepts that already exist in metamath. So don't be frustrated if your first proof takes you a month or more.
Over time, you level up by learning more concepts. You learn when to apply what theorem, You learn how to structure an informal proof in a metamath translatable way.
Eventually you will be level 70 and your boss is still a level 50 elephant, so now the proof takes you only a few hours instead of a month.
Then you can formalise harder challenges (i.e. higher level bosses) where again you'll need to learn new concepts.

Don't be discouraged though, although it is a very painful and arduous ride, you'll have lots of fun formalising the theorems you want.
You'll also gain a very detailed understanding of how mathematics actually works.

---

Your E-Mail. Your Cloud. Your Office. eclipso Mail Europe.

[Glauco]

Il giorno venerdì 4 luglio 2025 alle 13:02:22 UTC+2 alegr...@gmail.com 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 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).

[Jim Kingdon]

Here's one way to find that theorem. First I tried:

search * '( ( ? ^ ? ) ^ ? )'

(using metamath-exe). But then I remembered that ^ is for an integer exponent so I better try ^c instead. So the search

search * '( ( ? ^c ? ) ^c ? )'

finds cxpmul. That indeed has the restrictions described by Mario.

To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSsdjOPDC-BXUbRrEiH%2BA5A4sZbDYMgHjRHhoDSdV3Th6Q%40mail.gmail.com.

[Alessandro Griseta]

I see, thank you for pointing me to the correct resource, I'm starting to get the hang of metamath better now.