I was trying to prove the differential Bianchi identity by applying the covariant derivatives to each of the Riemann tensor terms
$R^{\lambda}_{\sigma\mu\nu;\rho}+R^{\lambda}_{\sigma\nu\rho;\mu}+R^{\lambda}_{\sigma\rho\mu;\nu}=0\space\space\space\space\space\space(1)$
and I got here:
$R^{\lambda}_{\sigma\mu\nu;\rho}=R^{\lambda}_{\sigma\mu\nu,\rho}+\Gamma^{\lambda}_{m\rho}R^{m}_{\sigma\mu\nu}-\Gamma^{m}_{\sigma\rho}R^{\lambda}_{m\mu\nu}-\Gamma^{m}_{\mu\rho}R^{\lambda}_{\sigma m\nu}-\Gamma^{m}_{\nu\rho}R^{\lambda}_{\sigma\mu m}\space\space\space\space\space(2)$
$R^{\lambda}_{\sigma\nu\rho;\mu}=R^{\lambda}_{\sigma\nu\rho,\mu}+\Gamma^{\lambda}_{m\mu}R^{m}_{\sigma\nu\rho}-\Gamma^{m}_{\sigma\mu}R^{\lambda}_{m\nu\rho}-\Gamma^{m}_{\nu\mu}R^{\lambda}_{\sigma m\rho}-\Gamma^{m}_{\rho\mu}R^{\lambda}_{\sigma\nu m}\space\space\space\space\space(3)$
$R^{\lambda}_{\sigma\rho\mu;\nu}=R^{\lambda}_{\sigma\rho\mu,\nu}+\Gamma^{\lambda}_{m\nu}R^{m}_{\sigma\rho\mu}-\Gamma^{m}_{\sigma\nu}R^{\lambda}_{m\rho\mu}-\Gamma^{m}_{\rho\nu}R^{\lambda}_{\sigma m\mu}-\Gamma^{m}_{\mu\nu}R^{\lambda}_{\sigma\rho m}\space\space\space\space\space\space(4)$
I know that using the torsion free property and the symmetries of the Riemann tensor, the last two terms of each of the equations (2),(3) and (4) when summed over cancel each other out. I dont know what to do from here in order to complete the proof.
Best Answer
Here is another proof. The covariant derivatives satisfy the Jacobi identity $$ [\nabla_\mu,[\nabla_\nu,\nabla_\kappa]]+ [\nabla_\nu,[\nabla_\kappa,\nabla_\mu]]+[\nabla_\kappa,[\nabla_\mu,\nabla_\nu]]=0. $$ This can be verified directly, but it is also known that pretty much any associative algebra will satisfy the Jacobi identity, and the elements $\nabla_1,...,\nabla_n$ basically generate a formal associative algebra.
Then letting the Jacobi identity act on any vector field $X^\rho$ we get for one of the terms $$ [\nabla_\kappa,[\nabla_\mu,\nabla_\nu]]X^\rho=\nabla_\kappa[\nabla_\mu,\nabla_\nu]X^\rho-[\nabla_\mu,\nabla_\nu]\nabla_\kappa X^\rho=\nabla_\kappa(R^\rho_{\ \sigma\mu\nu}X^\sigma)-R^\rho_{\ \sigma\mu\nu}\nabla_\kappa X^\sigma + R^\sigma_{\ \kappa\mu\nu}\nabla_\sigma X^\rho \\ =\nabla_\kappa R^\rho_{\ \sigma\mu\nu}X^\sigma+R^\rho_{\ \sigma\mu\nu}\nabla_\kappa X^\sigma-R^\rho_{\ \sigma\mu\nu}\nabla_\kappa X^\sigma+R^\sigma_{\ \kappa\mu\nu}\nabla_\sigma X^\rho \\ = \nabla_\kappa R^\rho_{\ \sigma\mu\nu}X^\sigma+R^\sigma_{\ \kappa\mu\nu}\nabla_\sigma X^\rho. $$
Now writing this into the Jacobi identity gives $$ 0=\left[\nabla_\kappa R^\rho_{\ \sigma\mu\nu}+\text{ cyclic permutations on }\kappa,\mu,\nu\right] X^\sigma+\left[R^\sigma_{\ \kappa\mu\nu}+\text{ cyclic permutations}\right]\nabla_\sigma X^\rho. $$
The second term here vanishes identically because of the algebraic Bianchi identity (cyclic identity), and what we are left with is the differential Bianchi identity.
Alternatively, this can be taken to be a proof of both the differential and algebraic Bianchi identity, since at any point $x$ one may take $$ X^\sigma(x)=\delta^\sigma_\alpha,\quad \nabla_\sigma X^\rho(x)=0, $$ which gives the differential Bianchi identity, and take $$ X^\sigma(x)=0,\quad \nabla_\sigma X^\rho(x)=\delta^\rho_\sigma, $$ which gives the algebraic Bianchi identity.
In this proof I have assumed torsionlessness, but the generalization to the torsionful case is similar, though more laborous.