How do I arrive at the multiplication function in lambda calculus? I'm familiar with how Church numerals are defined in the lambda calculus, i.e. as functions that take two arguments and apply the first argument $n$ times to the second.

Then I have the successor and addition functions, both of which I managed to derive and understand:

$$\begin{align}
\mathrm{succ} &amp;:= \lambda nsz.s (n s z) \\
(+) &amp;:= \lambda nm.n\ succ\ m \\
\end{align} $$

But multiplication is where I'm stuck.

I understand that we can define a multiplication function $(*)$ by adding the number $m$ to $0$ exactly $n$ times. After all, $3 \times 2$ is simply $2 + 2 + 2 + 0$.

So that could mean that $(*)$ looks like this:

$$(*) := \lambda nm.n\ ((+)\ m)\ 0$$

This appears to be a somewhat intuitive definition of a lambda calculus multiplication function to me, and if I try it out with $2$ and $3$, after some messy reductions, the result seems correct and $(*)\,2\,3 \rightarrow 6$.

But then elsewhere I found this definition for multiplication:

$$\mathrm{mult} := \lambda xya.x (y a)$$

Now I don't see how you arrive at this function $\mathrm{mult}$. My definition $(*)$, which takes two arguments, seems intuitive enough to me. But his here, which takes two arguments, one for the $x$ and $y$ respectively, which are the numbers to be multiplied, and then a third one $a$, just seems impenetrable to me—and I cannot figure out why it works, or how you would derive it.

Can somebody help me understand the reasoning and derivation of this $\mathrm{mult}$ function?
You know that $(\bar{n}\ s)$ corresponds to $s^{(n)}$, i.e. function $s$ applied $n$ times to its argument. You want to obtain a function that iterates some function $s$ exactly $n \cdot m$ times. From the above observations and some simple rules for the composition of functions we can immediately derive the body of $\textsf{mult}$:

$$s ^ {(n \cdot m)} =
\left( s ^ {(m)} \right) ^ {(n)} = 
\bar{n} \left(s ^ {(m)} \right) = 
\bar{n}\ (\bar{m}\ s) 
$$

Hence

$$ \textsf{mult}\ :=\ \overbrace{\lambda n m.}^\text{  parameters}\underbrace{(\lambda sz.n\ (m\ s) z)}_{\text{Church numeral}}$$

or, if we $\eta$-contract, we get

$$ \textsf{mult}\ :=\ \lambda nms.n\ (m\ s)$$