ZFC. How can we be so sure it formalizes big parts of math? I often hear people saying that all of mathematics can be formalized within ZFC. But I've also seen people who deny that, for example category theorists who work in an area where one might deal with say large categories. But everybody agrees that a large part of math (based on sets, not dealing with proper classes) can be formalized in ZFC.
Why can one be so sure? I mean, in practice we are using intuitive logic and set theory. Couldn't it be that we use an axiom of which we think it's obvious and evident, but which in fact isn't provable from ZFC?
 A: Not every mathematician cares much about formalization in ZFC -- but it's pretty much a given that every field of mathematics will have some mathematicians in it who are familiar enough with the ZFC formalism to be able to spot easily if some of its techniques could not be formalized there. With just a bit of experience you don't need to actually write the formalization down in all its mind-numbing detail to have an entirely reliable idea whether it can be done or not.
If these mathematicians did find such a problem, they would certainly make sure to make it known. No matter if you find a problem and also find a workaround for it, or you find a problem and after careful pondering can't see any way to fix it, the problem in itself would be an interesting and publishable result.
If such a discovery didn't lead to total loss of confidence in the affected results, reliable news that "here is an apparently useful theory other than category theory whose core techniques cannot be shoehorned into ZFC" would certainly spread quickly through the wider mathematics community.
