ZFC is the framework most contemporary mathematicians work in. However, some people don't like it. It's also possible that it is flawed some ways. Some people are working on new systems.
Related questions
@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.
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.