Most of us know the Jacobian conjecture. Here's a version below for fixed positive integers $d$ and $n$:

$J(d,n)$: If $f: C^n \rightarrow C^n$ is a polynomial map of degree $d$, and if the Jacobian determinant $\vert Jf \vert$ is nowhere vanishing (hence constant), then $f$ is injective (hence bijective).

We know that the sentence "For all $n$, $J(3,n)$" implies the sentence "For all $d,n$, $J(d,n)$." In other words, the Jacobian conjecture has been reduced to degree $3$.

We also know that, for any fixed $n$, $J(3,n)$ is provably true or provably false. This boils down to the completeness of the theory of algebraically closed fields of characteristic zero.

But, do we know whether the sentence "For all $n$, $J(3,n)$" is provably true or false? In other words, might the Jacobian conjecture be... (oh no).. undecidable?!

In other words, I could theoretically program my computer to set out to prove the Jacobian conjecture $J(3,1)$ (easy) and $J(3,2)$ then $J(3,3)$, etc.., and my theoretical computer would keep on going for epochs and epochs. But would it ever halt? Might this be undecidable?

anythingis undecidable in ZFC. However, it is conceivable that the undecidability of the conjecture in ZFC is provable by assuming some stronger hypothesis, such as the consistency of ZFC. $\endgroup$ – Emil Jeřábek May 17 '13 at 14:25