[proofplan]
We prove the formula by extracting coefficients from the Weyl character formula. The inverse denominator is expanded purely formally in the completed group algebra of the weight lattice, and its coefficients are precisely Kostant's partition function. For each Weyl group element $w$, the coefficient of $e^\mu$ is obtained by solving for the positive-root combination subtracted from $w(\lambda+\rho)-\rho$. Summing these signed contributions gives the stated multiplicity.
[/proofplan]
[step:Write the Weyl character formula in shifted denominator form]
Let $\mathbb Z[P]$ denote the integral group algebra with basis elements $e^\nu$ indexed by $\nu\in P$, with multiplication determined by
\begin{align*}
e^\nu e^\eta=e^{\nu+\eta}
\end{align*}
for $\nu,\eta\in P$. We use the standard formal-character notation
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{\eta\in P}\dim L(\lambda)_\eta e^\eta.
\end{align*}
The hypotheses of the [Weyl Character Formula]([citetheorem:9384]) are satisfied: $\mathfrak g$ is finite-dimensional complex semisimple, $\mathfrak h$ is a Cartan subalgebra, $\Phi^+$ is a chosen positive system, $\lambda\in P^+$ is dominant integral, and $L(\lambda)$ is the irreducible finite-dimensional highest weight module of highest weight $\lambda$. Since $\rho\in P$ and $W$ preserves $P$, all formal exponents below lie in $P$. The formula gives
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{w\in W}\det(w)e^{w(\lambda+\rho)-\rho}\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})^{-1}.
\end{align*}
This identity is interpreted in the formal completion of $\mathbb Z[P]$ in the negative root directions, so the product is a formal [power series](/page/Power%20Series) rather than an analytic product.
[/step]
[step:Expand the inverse denominator using Kostant's partition function]
For each positive root $\alpha\in\Phi^+$, expand the factor $(1-e^{-\alpha})^{-1}$ as the formal geometric series
\begin{align*}
(1-e^{-\alpha})^{-1}=\sum_{n=0}^{\infty}e^{-n\alpha}.
\end{align*}
Multiplying these formal series over the finite set $\Phi^+$ gives
\begin{align*}
\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})^{-1}
=
\sum_{(n_\alpha)_{\alpha\in\Phi^+}\in\mathbb Z_{\ge 0}^{\Phi^+}}
e^{-\sum_{\alpha\in\Phi^+}n_\alpha\alpha}.
\end{align*}
By the definition of $p$, the coefficient of $e^{-\nu}$ in this product is $p(\nu)$. Hence
\begin{align*}
\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})^{-1}
=
\sum_{\nu\in P}p(\nu)e^{-\nu}.
\end{align*}
[guided]
The denominator product must be handled as a formal object. For one positive root $\alpha$, the inverse factor is expanded by the formal geometric identity
\begin{align*}
(1-e^{-\alpha})^{-1}=\sum_{n=0}^{\infty}e^{-n\alpha}.
\end{align*}
No convergence is being asserted here. The expression lives in the completion where weights may be shifted arbitrarily far in the nonpositive span of the positive roots.
Now multiply these expansions over the finite set $\Phi^+$. Choosing one term from each factor is the same thing as choosing a family of nonnegative integers
\begin{align*}
(n_\alpha)_{\alpha\in\Phi^+}\in\mathbb Z_{\ge 0}^{\Phi^+}.
\end{align*}
The corresponding monomial is
\begin{align*}
\prod_{\alpha\in\Phi^+}e^{-n_\alpha\alpha}=e^{-\sum_{\alpha\in\Phi^+}n_\alpha\alpha}.
\end{align*}
Therefore
\begin{align*}
\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})^{-1}
=
\sum_{(n_\alpha)_{\alpha\in\Phi^+}\in\mathbb Z_{\ge 0}^{\Phi^+}}
e^{-\sum_{\alpha\in\Phi^+}n_\alpha\alpha}.
\end{align*}
The coefficient of $e^{-\nu}$ is exactly the number of choices of the family $(n_\alpha)_{\alpha\in\Phi^+}$ for which
\begin{align*}
\nu=\sum_{\alpha\in\Phi^+}n_\alpha\alpha.
\end{align*}
By definition, this number is $p(\nu)$. If no such family exists, then the coefficient is zero, which is also how $p(\nu)$ is defined. Thus the whole inverse denominator is
\begin{align*}
\prod_{\alpha\in\Phi^+}(1-e^{-\alpha})^{-1}
=
\sum_{\nu\in P}p(\nu)e^{-\nu}.
\end{align*}
[/guided]
[/step]
[step:Extract the coefficient of a fixed weight]
Substituting the expansion from the previous step into the Weyl character formula gives
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{w\in W}\det(w)e^{w(\lambda+\rho)-\rho}\sum_{\nu\in P}p(\nu)e^{-\nu}.
\end{align*}
For fixed $w\in W$ and $\nu\in P$, the corresponding term is
\begin{align*}
\det(w)p(\nu)e^{w(\lambda+\rho)-\rho-\nu}.
\end{align*}
This term contributes to the coefficient of $e^\mu$ exactly when
\begin{align*}
\mu=w(\lambda+\rho)-\rho-\nu.
\end{align*}
Equivalently,
\begin{align*}
\nu=w(\lambda+\rho)-(\mu+\rho).
\end{align*}
Thus, for this fixed $w$, the contribution to the coefficient of $e^\mu$ is
\begin{align*}
\det(w)p\bigl(w(\lambda+\rho)-(\mu+\rho)\bigr).
\end{align*}
[/step]
[step:Identify the coefficient with the weight multiplicity]
By the definition of the formal character,
\begin{align*}
\operatorname{ch}L(\lambda)=\sum_{\eta\in P}\dim L(\lambda)_\eta e^\eta.
\end{align*}
Therefore the coefficient of $e^\mu$ in $\operatorname{ch}L(\lambda)$ is $\dim L(\lambda)_\mu$. Summing the coefficient contributions from all $w\in W$ gives
\begin{align*}
\dim L(\lambda)_\mu=\sum_{w\in W}\det(w)p\bigl(w(\lambda+\rho)-(\mu+\rho)\bigr).
\end{align*}
This is the asserted Kostant [multiplicity formula](/theorems/2420).
[/step]
