non commutative polynomial which is zero for all matrix evaluation Let $K$ be a (commutative) field.
We can define the free $K$-algebra of polynomials in non commutative variables $x_1, \cdots, x_n$. It 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 $n$-tuple of $m\times m$-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.

*

*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.


*Algebras ${\rm M}_m(K)$ are polynomial identity 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$ . Here we assume that the matrices $M_1, \cdots, M_n$ have to be jointly nilpotent (i.e., any sufficiently long product $M_{i_1} M_{i_2} \cdots M_{i_k}$ is $0$).
 A: The answer is yes.
It suffices to note that for any $n$ and $d$, there are matrices $M_1,\dots,M_n$ of the same dimension $m$ such that the set of all the products $M_{i_1}\cdots M_{i_e}$ for $1\le i_1,\dots,i_e\le n$, $0\le e\le d$, is linearly independent. One possible choice is to take $m$ to be the number of nodes in the complete $n$-ary tree $T$ of height $d+1$, and $M_i$ to be the permutation matrix corresponding to the function $T\to T$ that maps each non-leaf node to its $i$-th child (and leaves anywhere).
A: This is an algebraic elaboration on Emil's answer.
Let $A = K \langle x_1,\ldots,x_n \rangle$ and let $\hat{A} = K \langle\langle x_1,\ldots, x_n \rangle \rangle$. Since $A$ is a subring of $\hat{A}$, a positive answer for $\hat{A}$ implies one for $A$.
Now for each $d \in \mathbb{N}$, let $\hat{A}_{d}$ be the $K$-linear span of all products of the generators $x_1,\ldots, x_n$ of length exactly $d$. Then $\hat{A}_{d} \cdot \hat{A}_e = \hat{A}_{d+e}$ for all $d,e\in\mathbb{N}$, and there is a vector space isomorphism
$$\prod_{d=0}^\infty \hat{A}_d \stackrel{\cong}{\longrightarrow} \hat{A}.$$
This just says that every non-commutative formal power series can be uniquely decomposed as an infinite (convergent in a natural topology on $\hat{A}$) sum of its homogeneous components.
Now let $\hat{A}_{>m} := \prod_{d>m} \hat{A}_d$ for each $m \geq 0$. These are two-sided ideals of $\hat{A}$, and for each $m \geq 0$,
$$V_m := \hat{A} / \hat{A}_{>m} \cong \prod_{d=0}^m \hat{A}_d$$
is a finite dimensional vector space over $K$, of dimension $N_m$, say. This gives us matrix representations 
$$\rho_m : \hat{A} \to End_K(V_m) \cong M_{N_m}(K).$$
Clearly $\hat{A}_{> m}$ is contained in $\ker \rho_m$, but in fact we have equality, because $\hat{A} / \hat{A}_{>m}$ (being an associative $K$-algebra in its own right) acts faithfully on itself by left multiplication.
So if $P \in \hat{A}$ is zero on every set of $n$ matrices of size $N$ for all $N \geq 0$, then we see that in particular, $P \in \ker \rho_m$ for all $m \geq 0$. Hence $P \in \bigcap_{m \geq 0} \hat{A}_{>m}$, which implies that every homogeneous component of $P$ is zero. Hence $P$ is also zero.
