I want to work on $K$ an algebraic closed (commutative) field of characteristic zero (even if it seems to be more general). We can define the free K-algebra of polynomials in non commutative variables $x_1, \cdots, x_n$. Il is usually denoted by $K\langle x_1, \cdots, x_n \rangle$.
Fix a non commutative polynomial $P \in K\langle x_1, \cdots, x_n \rangle$. For every natural number $m$ and every choice of matrices $M_1, \cdots, M_n \in {\rm M}_m(K)$, we can evaluate $P$ at $(M_1, \cdots, M_n)$ to obtain a matrix $P(M_1, \cdots, M_n) \in {\rm M}_m(K)$.
My question is : if the evaluation of $P$ on every matrices $(M_1, \cdots, M_n)$ for every $m$ is $0$, is necessary $P = 0 \in K\langle x_1, \cdots, x_n \rangle$ ?
I don't know if the question is totally trivial.
1) In fact, if we restrict the condition to $m=1$, the answer is clearly no because the non commutative polynomial $x_1 x_2 - x_2 x_1$ for example is non zero. But it is yes if we consider polynomial in commutative variables.
2) Algebras ${\rm M}_m(K)$ are polynomial rings. In particular, the answer is no again if the condition $P(M_1, \cdots, M_n) =0$ only for all $M_1, \cdots, M_n \in {\rm M}_m(K)$ for a fixed $m$. Amitsur–Levitzki theorem gives an explicit counter-example.
Extension of the question : same question where we replace $P \in K\langle x_1, \cdots, x_n \rangle$ by a non commutative formal power series $S \in K\langle\langle x_1, \cdots, x_n \rangle\rangle$ .
Thanks a lot for yours answers.