Comment by Garlef

> but cannot prove more theorems

usually you're more interested in better ergonomics: can you do X with less work?

it's like picking a programming language - depending on what you're attempting, some will be more helpful.

and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code"

the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.