The dependence on AC through the use of Zorn's lemma in the proof of the Choquet–Bruhat–Geroch theorem on the existence of a maximal globally hyperbolic development for solutions of the Einstein equations has been eliminated around the same time by Jan Sbierski, in On the Existence of a Maximal Cauchy Development for the Einstein Equations — a Dezornification, and Willie Wong, in A comment on the construction of the maximal globally hyperbolic Cauchy development (the latter having been mentioned by Asaf Karagila in the comments).
More generally, an analogous, but non-exhaustive, discussion has appeared earlier over at M.SE10102 and MO45928 in the context of Riemannian geometry.
The conclusion seems to be that several fundamental results in functional analysis anyway use the axiom of choice or some version of it. Mathematical GR certainly uses the theory of linear (and nonlinear) elliptic and hyperbolic PDEs, which in particular relies on the theory of Sobolev spaces (and possibly also Schwartz distributions). The basic results where (to my knowledge) AC creeps in include
- the Hahn–Banach theorem,
- the countable additivity of Lebesgue measure (may be used in Sobolev theory),
- the Arzelà–Ascoli and Fréchet–Kolmogorov theorems (used in Sobolev embeddings),
- the Banach–Alaoglu theorem (as a step in applying Schauder-like fixed-point theorems),
- the uniform boundedness principle,
- and maybe others.
Most likely, the list is non-exhaustive. From the notes Zornian Functional Analysis or: How I Learned to Stop Worrying and Love the Axiom of Choice by Asaf Karagila and the answer by Cloudscape to MO45928, it seems that there are versions of these theorems that do not require AC under some hypothesis (like restricting to separable Banach spaces) or only a weakend version of it (like countable choice). I guess that it might be an open question, whether all of this dependence on AC could be eliminated sufficiently reasonable hypothesis (say sufficient for the mathematical study of gravitational waves from astrophysical sources). If one could write a reasonable textbook on PDE theory without AC, then probably one could adapt the same methods to Mathematical GR.
For reference, below is the currently functional link to the online database of the consequence of AC. Not all the above theorems appear there by name, but maybe only in some equivalent version (cf. the previously mentioned M.SE and MO discussions).
