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.)



Does anyone know a polynomial whose lack of roots can't be proved?
In his Master's Thesis, Merlin Carl has computed a polynomial that is solvable in the integers iff ZFC is inconsistent. A joint paper with his advisor Boris Moroz on this subject can be found at <http://www.math.uni-bonn.de/people/carl/preprint.pdf>.


