Does anyone know a polynomial whose lack of roots can't be proved? In Ebbinghaus-Flum-Thomas's Introduction to Mathematical Logic, the following  assertion is made:
If ZFC is consistent, then one can obtain a  polynomial $P(x_1, ..., x_n)$ which has no roots in the integers. However, this cannot be proved (within ZFC).
So if $P$ has no roots, then mathematics (=ZFC, for now) cannot prove it.
The justification is that Matiyasevich's solution to Hilbert's tenth problem allows one to turn statements about provable truths in a formal system to the existence of integer roots to polynomial equations.  The statement is "ZFC is consistent," which cannot be proved within ZFC thanks to Gödel's theorem.
Question: Has such a polynomial ever been computed?
(This arose in a comment thread on the beta site math.SE.)

For every consistent recursively axiomatizable theory $T$ there exists (and can be effectively computed from the axioms of $T$) an integer number $K$ such that the following Diophantine equation (where all letters except $K$ are variables) has no solutions over non-negative integers, but this fact cannot be proved in $T$:
\begin{align}&(elg^2 + \alpha - bq^2)^2 + (q - b^{5^{60}})^2 + (\lambda + q^4 - 1 - \lambda b^5)^2 + \\
&(\theta + 2z - b^5)^2 + (u + t \theta - l)^2 + (y + m \theta - e)^2 + (n - q^{16})^2 + \\
&[(g + eq^3 + lq^5 + (2(e - z \lambda)(1 + g)^4 + \lambda b^5 + \lambda b^5 q^4)q^4)(n^2 - n) + \\
&\quad\quad(q^3 - bl + l + \theta \lambda q^3 + (b^5-2)q^5)(n^2 - 1) - r]^2 + \\
&(p - 2w s^2 r^2 n^2)^2 + (p^2 k^2 - k^2 + 1 - \tau^2)^2 + \\
&(4(c - ksn^2)^2 + \eta - k^2)^2 + (r + 1 + hp - h - k)^2 + \\
&(a - (wn^2 + 1)rsn^2)^2 + (2r + 1 + \phi - c)^2 + \\
&(bw + ca - 2c + 4\alpha \gamma - 5\gamma - d)^2 + \\
&((a^2 - 1)c^2 + 1 - d^2)^2 + ((a^2 - 1)i^2c^4 + 1 - f^2)^2 + \\
&(((a + f^2(d^2 - a))^2 - 1) (2r + 1 + jc)^2 + 1 - (d + of)^2)^2 + \\
&(((z+u+y)^2+u)^2 + y-K)^2 = 0.
\end{align}
Moreover, for every such theory, the set of numbers with this property is infinite and not recursively enumerable.
The equation is derived from Undecidable Diophantine Equations, James P. Jones, Bull. Amer. Math. Soc. (N.S.), Vol. 3(2), Sep. 1980, pp. 859–862, DOI: 10.1090/S0273-0979-1980-14832-6.
