Very interesting question!

Here's the only thing I can think of:

A large portion of mathematics starts being done in proof assistants / with AI / ??? and for some technical reason it turns out another foundation is better for that?

@jacksonpolack Good point. I'm no expert, but I think the most popular proof assistants right now don't use ZFC as their foundation, but instead some kind of type theoretic foundation. Some discussion about this can be found in
- The paper The Lean Mathematical Library
- MathOverflow: What makes dependent type theory more suitable than set theory for proof assistants?

I assume if human mathematicians are replaced by AIs, and the AIs work in something like type theory, this question resolves YES?

I think this will happen. Math can be fully formalized and computer verified, so you could probably train an AI to become very good at math by self-play. And ZFC isn't a great foundation for fully formal math, so when it happens it probably won't use ZFC.

@tailcalled Yeah.

Historically, it seems that Ernst Zermelo first formulated a so-called "Zermelo set theory" in 1908 (see this Encyclopedia Britannica article), and then Abraham Fraenkel modified it in 1922(?) to produce the modern Zermelo-Fraenkel set theory. Since ZFC has been around as an idea for the past 101 years, I doubt it'll get dethroned in the next 27.