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?