OK, I know that Matiyasevich's solution to Hilbert's 10th problem shows that there is no algorithm to decide whether or not a polynomial $p(x_1,\ldots,p_n)$ with integer coefficients has a solution over the integers. I have no doubts about the truth of that. However, I have been unable to figure out why the following algorithm doesn't work.
Program one computer to plug every $(x_1,\ldots,x_n) \in \mathbb{Z}^n$ into $p(x_1,\ldots,p_n)$. If there is an integer solution, then this will halt eventually. Program a second computer to enumerate every possible proof. There are only countably many, so if there is a proof that $p(x_1,\ldots,x_n)$ has no integer solutions, then this computer will eventually find one.
Given Matiyasevich's theorem, the only conclusion I can draw is that there are polynomials that don't have integral zeros, but for which there is no proof that they don't (so it's independent of ZFC). This seems very odd to me. What am I missing?
(Usual disclaimers about ZFC being consistent, etc.)
You are not missing anything, this is precisely the case. For example, there is a polynomial $p(x_1,\dots,x_n)\in{\mathbb Z}[x_1,\dots,x_n]$ for some $n$ so that any integer solution codes a proof that ZFC is inconsistent. There are no integer solutions, and there are no proofs in ZFC of this fact. The point is that the 10th problem shows that the r.e. sets are precisely the Diophantine sets.