We introduce three formal theories of increasing strength for
linear algebra in order to study the complexity of the concepts
needed to prove the basic theorems of the subject. We give
what is apparently the first feasible proofs of the Cayley-Hamilton
theorem and other properties of the determinant, and study the
propositional proof complexity of matrix identities.