  We give a computational approach to theorem proving in homological algebra.
This approach is based on computations in the free abelian category of an
additive category $\mathbf{A}$. We show that the free abelian category is
amenable to explicit computations whenever we can decide homotopy equations in
$\mathbf{A}$. As some consequences of our investigations, we recover Dowker's
explicit formula for the connecting homomorphism $\partial$ in the snake lemma,
we find a universal sense in which $\partial$ is unique, and we give a refined
version of the 5-lemma.
