Does there exist a formal statement of the Multivariable Factor Theorem? I've been searching around for a formal definition, but I haven't found one yet. There are a few examples of how to use it, namely here. I've been playing around with possible statements myself, and I've come up with two candidates, the second a generalization of the first. I'll phrase each in terms of polynomials in $\mathbb{C}[x,y,z]$ because they're easily generalizable to $n$ variables if true.

If $f(x,y,z)$ is a polynomial, and $P(y,z)$ is a polynomial satisfying $f(P(y,z),y,z)=0$ for all complex $y$ and $z$, then $x-P(y,z)$ is a factor of $f(x,y,z)$.

This one I think I've successfully shown, just by using the remainder theorem where the remainder is designated to have smaller $x$-degree.

If $f(x,y,z)$ and $P(x,y,z)$ are polynomials such that for any $x,y,z\in\mathbb{C}$ the following implication holds:
  $$P(x,y,z)=0\Longrightarrow f(x,y,z)=0,$$
  then $P(x,y,z)$ is a factor of $f(x,y,z)$.

This I have less of an idea how to show, because the remainder theorem is trickier for multivariable polynomials. It still looks true to me.
 A: Theorems typically can be stated in many different ways, and so there usually isn't any single "correct" version but instead several closely related statements you might see in different contexts.  The term "multivariable factor theorem" is also not a particularly standard name for any theorem.  Your first statement is a perfectly reasonable and correct statement of a theorem which could have that name, though (assuming all your polynomials have complex coefficients).  In a more abstract context, there is also the following generalization:

If $R$ is a commutative ring, $r\in R$, and $f(x)\in R[x]$ is a polynomial such that $f(r)=0$, then $x-r$ is a factor of $f(x)$.

This can be proved by the usual long division argument that shows that $f(r)$ is the remainder when you divide $f(x)$ by $x-r$.  Your version can then be deduced by just considering $R=\mathbb{C}[y,z]$ and $r=P(y,z)$ (note that this uses the fact that if the polynomial $g(y,z)=f(P(y,z),y,z)$ vanishes for all $y,z\in\mathbb{C}$ then in fact $g$ is the zero polynomial).

There's a good reason you haven't managed to prove your second statement: it's not true!  For instance, $P(x,y,z)=x^2$ and $f(x,y,z)=x$ is a counterexample.  It is true if you assume additionally that $P$ is square-free: that is, it has no repeated irreducible factors.  This is more difficult to prove than your first statement, though.  As evidence that this result is considerably deeper than just facts about polynomial division, note that taking $f=1$, it implies that any non-constant $P$ must have a zero, and so in particular it implies the fundamental theorem of algebra.  It is a special case of a much more general hard theorem known as the Nullstellensatz.
Here is the most elementary proof I can come up with for it.  I will state it a bit more generally (and also in a way that requires you to already know the fundamental theorem of algebra in order to apply it to $\mathbb{C}$):

Theorem (Nullstellensatz for principal ideals): Let $k$ be an algebraically closed field and let $f,P\in k[x_1,\dots,x_n]$ where $P$ is squarefree.  Suppose that for all $a\in k^n$, $P(a)=0$ implies $f(a)=0$.  Then $P$ divides $f$.

Proof: Using unique factorization in $k[x_1,\dots,x_n]$, it suffices to show each irreducible factor of $P$ divides $f$, so we may assume $P$ is irreducible.  We assume without loss of generality that the variable $x_1$ appears in $P$.  Let $A=k[x_2,\dots,x_n]$ and let $K$ be its field of fractions $k(x_2,\dots,x_n)$; we will think of our polynomial ring as $A[x_1]$.  Using the Euclidean algorithm over $K$, we find the GCD $g$ of $f$ and $P$ in $K[x_1]$, which divides both $f$ and $P$ in $K[x_1]$ and also can be written as $rf+sP$ for some $r,s\in K[x_1]$.  Clearing denominators and dividing out any common factors of the coefficients of $g$, we may assume that actually $g\in A[x_1]$ and that $g$ has no nontrivial factors in $A$.  Since $A$ is a UFD, Gauss's lemma now implies that since $g$ divides $P$ and $f$ in $K[x_1]$, it actually also divides $P$ and $f$ in $A[x_1]$.  Since $P$ is irreducible, this implies either $g$ is a  nonzero constant or $g$ is a nonzero constant multiple of $P$.  If $g$ is a nonzero constant multiple of $P$, then since $g$ divides $f$ we conclude that $P$ divides $f$ and are done.
If instead $g$ is a nonzero constant, then we can use the equation $$rf+sP=g$$ as well as our other hypotheses to reach a contradiction.  Let $t\in A$ be a common denominator of $r$ and $s$ and let $u\in A$ be the leading coefficient of $P$, considered as an element of $A[x_1]$.  Since $k$ is infinite and $t$ and $u$ are nonzero, we can choose $b\in k^{n-1}$ such that $t(b)u(b)\neq 0$.  Substituting $b$ for $(x_2,\dots,x_n)$ in $P$, we get a nonconstant polynomial $P_b(x_1)\in k[x_1]$ (here we use the assumption that $x_1$ appears in $P$).  Since $k$ is algebraically closed, $P_b$ has a root $c\in k$.  Now letting $a=(c,b)\in k^n$, we have $P(a)=0$, so by hypothesis $f(a)=0$ as well.  Since $t(b)\neq 0$, we can also evaluate $r(b)$ and $s(b)$ and so can substitute $a$ into the equation $rf+sP=g$ to find that the left side is $0$ and the right side is nonzero.  This is a contradiction, and completes the proof.
