A friend of mine is a differential geometer, and keeps insisting that he doesn't need the axiom of choice for the things he does. I'm fairly certain that's not true, though I haven't dug into the details of Riemannian geometry (or the real analysis it's based on, or the topology, or the theory of vector spaces, etc…) to try and find a theorem or construction that uses the axiom of choice, or one of its logical equivalences.
So do you know of any result in Riemannian geometry that needs the axiom of choice? They should be there somewhere, I particularily suspect that one or more is hidden in the basic topology results one uses.
Best Answer
It is very possible that your colleague generally avoids using the axiom of choice, because manifolds are relatively concrete objects. Assuming that your friend is studying only separable manifolds, or better yet only compact ones, that makes it possible to do many constructions very explicitly, without using the axiom of choice. This is similar to the way that various principles of analysis that require the axiom of choice in general do not require the axiom of choice when they are applied to Euclidean spaces.
So you're right that it may be easier to find AC in the background results. The trouble is that many of these background results are studied in far more generality than they are used. For example, suppose an analyst uses the fact that $[0,1]\times[0,1]$ is compact. This fact follows from Tychonoff's theorem, which for general topological spaces does require the axiom of choice. But we could prove the compactness of the unit square more directly, avoiding the axiom of choice altogether (this relies on the separability of the square, in particular).
So sometimes the axiom of choice is used for convenience, by the invocation of a very general result, but it could be avoided if necessary. If we were to study only smooth manifolds that had already been embedded into Euclidean space, I suspect that we would be able to do pretty much everything in Zermelo-Fraenkel set theory without the axiom of choice. But it would take careful attention in the proofs to make sure that we replace choice-based techniques with alternative methods.
I know this isn't a direct answer to the question, but I think it's relevant since it explains a caveat with possible answers: just because a general result requires AC doesn't mean that AC is required for all consequences of that result.