# Algorithms to prove that polynomials don't have integer solutions

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?

-
It is indeed very odd. But true. (I did once slog through the proof of Matiyasevich's theorem, when I was young. My advice to you is to take it on trust.) – TonyK Dec 23 '10 at 19:28
@TonyK : This is sad advice. The proof is very nice. Plus, there is a lot of very active work in number theory extending it. – Andrés E. Caicedo Dec 23 '10 at 21:24
@Andres Caicedo: Maybe the proof has been improved since 1981! – TonyK Dec 23 '10 at 22:15
@TonyK: I very much like the presentation in Matiyasevich's book "Hilbert's Tenth Problem", The MIT Press, Cambridge, London, 1993. For modern work and current lines of research, you may want to take a look at "Hilbert’s Tenth Problem: Diophantine Classes and Other Extensions to Global Fields" by Alexandra Shlapentokh, Cambridge University Press, 2006. – Andrés E. Caicedo Dec 23 '10 at 22:36

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.