Solution (source code)

= Solution

Lower the free index of $K$. The <Killing equation> makes the last two indices of $\nabla_\nu\nabla_\mu K_\alpha$ antisymmetric after the appropriate derivative is moved. Combining the three resulting <Ricci identities> cyclically gives
$$
\nabla_\nu\nabla_\mu K_\alpha
=\frac12\left(
[\nabla_\nu,\nabla_\mu]K_\alpha
-[\nabla_\mu,\nabla_\alpha]K_\nu
+[\nabla_\alpha,\nabla_\nu]K_\mu
\right).
$$
Applying the covector form of the Ricci identity and then the <first Bianchi identity> reduces this to
$$
\nabla_\nu\nabla_\mu K_\alpha
=R_{\alpha\mu\nu\beta}K^\beta.
$$
Raising $\alpha$ proves the <second covariant derivative of a Killing vector> identity
$$
\boxed{\nabla_\nu\nabla_\mu K^\alpha
=R^\alpha{}_{\mu\nu\beta}K^\beta.}
$$
Contracting $\mu$ and $\nu$ and using the definition and symmetries of the <Ricci tensor> gives
$$
\boxed{\nabla_\mu\nabla^\mu K^\alpha
=-R^\alpha{}_{\beta}K^\beta.}
$$