Motivated by the fundamental lower bounds questions in proof complexity, we investigate the complexity of generating identities of matrix rings, and related problems. Specifically, for a field F let A be a non-commutative (associative) F-algebra (e.g., the algebra Matd(F) of dd matrices over F). We say that a non-commutative polynomial f(x1xn) over F is an identity of A, if for all cAn, f(c)=0. Let B be a set of non-commutative polynomials that forms a basis for the identities of A, in the following sense: for every identity f of A there exist non-commutative polynomials g1gk , for some k, that are substitution instances of polynomials from B, such that f is in the (two-sided) ideal g1gk . We study the following question: Given AB and f as above, what is the minimal number k of such generators g1gk for which fg1gk ?

In particular, we focus on the case where the algebra A is Matd(F), and F has characteristic 0. Our main technical contribution is a generalization of the lower bound presented in Hrubes (2011) (for the case d=1) to any 2">d2:

For every natural number 2">d2 and every finite basis B for the identities of Matd(F), where F is of characteristic 0, there exists an identity fn with n variables, that requires (n2d) generators (i.e., substitution instances from B) to generate.

Note that for any 2">d2, it is an open problem to find a basis for the identities of Matd(F) (while the existence of a finite basis was proved by Kemer (1987)). Nevertheless, using results from the theory of algebras with polynomial identities (PI-algebras) together with a generalization of the arguments in Hrubes (2011), we conclude the above lower bound for every finite basis B.We then explore connections to lower bounds in proof complexity. We consider arithmetic proofs of polynomial identities that operate with algebraic circuits and whose axioms are the polynomial-ring axioms (which can be considered as an algebraic analogue of the Extended Frege propositional proof system). We raise the following basic question: is it true that using the generators of the (non-commutative) polynomial identities over Matd(F) as axiom (schemes) is an optimal way to prove such identities, with respect to proof size? Namely, is it true that proving matrix identities by reasoning with polynomials whose variables X1Xn range over matrices is as efficient as proving matrix identities using polynomials whose variables range over the *entries* of the matrices X1Xn ? We show that a positive answer to this question may lead, under further assumptions (which are generalization of the assumptions presented in Hrubes (2011)), up to exponential-size lower bounds on arithmetic proofs.