Solution (source code)

= Solution

Choose a <Borel subalgebra> $\mathfrak b=\mathfrak t\oplus\mathfrak n^+$. For $\lambda\in\mathfrak t^*$, let $\mathbb C_\lambda$ be the one-dimensional $\mathfrak b$-module on which $\mathfrak n^+$ acts by zero and $h\in\mathfrak t$ acts by $\lambda(h)$. The <Verma module> is
$$
M(\lambda)=U(\mathfrak g)\otimes_{U(\mathfrak b)}\mathbb C_\lambda.
$$
Its <universal property of a Verma module> says that any vector of weight $\lambda$ annihilated by $\mathfrak n^+$ receives the canonical highest-weight vector under one unique module homomorphism from $M(\lambda)$.

The sum of the proper submodules of $M(\lambda)$ is its unique maximal proper submodule, because no proper submodule contains the highest-weight vector. Its quotient $V(\lambda)$ is therefore the unique <irreducible quotient of a Verma module>, and hence the unique irreducible highest-weight module of weight $\lambda$.

The module $V(\lambda)$ is finite-dimensional exactly when $\lambda$ is a <dominant integral weight>:
$$
\langle\lambda,\alpha_i^\vee\rangle\in\mathbb Z_{\geq0}
$$
for every simple root $\alpha_i$.