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?