  Motivated by the fundamental lower bounds questions in proof complexity, we
initiate the study of matrix identities as hard instances for strong proof
systems. A matrix identity of $d \times d$ matrices over a field $\mathbb{F}$,
is a non-commutative polynomial $f(x_1,\ldots,x_n)$ over $\mathbb{F}$ such that
$f$ vanishes on every $d \times d$ matrix assignment to its variables.
  We focus on arithmetic proofs, which are proofs of polynomial identities
operating with arithmetic circuits and whose axioms are the polynomial-ring
axioms (these proofs serve as an algebraic analogue of the Extended Frege
propositional proof system; and over $GF(2)$ they constitute formally a
sub-system of Extended Frege [HT12]). We introduce a decreasing in strength
hierarchy of proof systems within arithmetic proofs, in which the $d$th level
is a sound and complete proof system for proving $d \times d$ matrix identities
(over a given field). For each level $d>2$ in the hierarchy, we establish a
proof-size lower bound in terms of the number of variables in the matrix
identity proved: we show the existence of a family of matrix identities $f_n$
with $n$ variables, such that any proof of $f_n=0$ requires $\Omega(n^{2d})$
number of lines. The lower bound argument uses fundamental results from the
theory of algebras with polynomial identities together with a generalization of
the arguments in [Hru11].
  We then set out to study matrix identities as hard instances for (full)
arithmetic proofs. We present two conjectures, one about non-commutative
arithmetic circuit complexity and the other about proof complexity, under which
up to exponential-size lower bounds on arithmetic proofs (in terms of the
arithmetic circuit size of the identities proved) hold. Finally, we discuss the
applicability of our approach to strong propositional proof systems such as
Extended Frege.
