Statements in differential geometry independent from ZFC It is well known that some problems in functional analysis and in general topology are independent from ZFC: to name a few, Kaplansky's conjecture, the existence of outer automorphisms of the Calkin algebra, the existence of a Suslin line etc. This is not too surprising, since many results in this fields require a nontrivial amount of set theory to be proved. On the other hand, differential geometry seems to be "higher up" in mathematical complexity (i.e., further away from set theoretical questions) and so it seems reasonable to me that no "natural" statement in diff. geom. is independent from ZFC.
Is that the case? That is, are there some statements which are independent from ZFC (or are conjectured to be)?
Edit: many comments (and the only, at the moment, answer) focused on computably undecidable problems. While this does indeed answer the question as formulated (because at least one instance of the problem must be independent), it is not exactly what I had in mind in that it does not offer an explicit example of an independent statement, or at least I don't see how to get one. So a more precise reformulation of my question is (but I am also very interested in more examples of computably indecidable problems): is there an explicit (in some sense of the word) statement in differential geometry that is (or is conjectured to be) independent from ZFC?
 A: An explicit construction from the undecidability problem is this. There is a computer program $C$ that can check whether a (completely formal) proof in ZFC is valid, i.e. whether each step is either an axiom or follows from previous steps by a set of logical rules. Proofs are simply finite length strings drawn from a finite alphabet, so there is a program $S$ that outputs every (valid or invalid) proof one by one, ordered by length and alphabetical order. Now use $C$ to filter out the invalid proofs. This gives you a program that outputs every valid proof. Program $H$ runs through every proof, and when it encounters a proof of $p \land \neg p$, it halts. All of these are very easy but tedious to write out, if you have some basic programming knowledge. Whether this program halts is obviously independent of ZFC.
There is a very constructive proof that constructs a finite presentation of a group, such that whether a particular element $w$ is equal to the identity is equivalent to some program halting. This is done by using a lot of generators to guard the boundaries of symbols, so that there is only one potential path of equational reasoning that the given element is the identity. This path mimics the execution of a program. This construction is explicit, and you can check all the construction details if you have enough time.
Finally, there are ways to construct a 4-manifold for any given finite presentation of a group, so that it is diffeomorphic to another 4-manifold if and only if adding the equation $w = 1$ gives an isomorphic group. This result is mentioned in the comments.
A: [Using the comments for context on undecidability/independence of ZFC]
A computably undecidable problem is whether or not a homology sphere has a metric of positive scalar curvature [Page 79 of Computers, Rigidity, and Moduli].
