I don't understand arguments like "nobody can agree on what set theory is". This is not how mathematics work.

In mathematics labels are _not_ important, definitions are.

One simple example that everybody can relate to: do natural numbers include 0 or not? Who cares? Some definitions include it, some do not. There's even a convention of using N for N with 0, and N+ for excluding it, but even the convention is just a convention, not a definition. You could call them "funky numbers, the set of whole positive numbers including 0", and you're fine. Funky, natural, those are just names, labels, as long as you define them, it doesn't matter.

Same applies to set theory, there's many, many set theories, and they differ between properties, and this has never caused problems, because in mathematical discussion or literature...you provide or point to a definition. So you'll never discuss about "set theory" without providing one or pointing to one.

This is very, very different from how normal people waste their time.

E.g. arguing whether AI "thinks" or not, but never defining what thinking means, thus you can't even conclude whether you think or not, because it's never been defined.

The distinction between material set theories (like ZF and other set-theoretical foundations you might have heard about) and structural set theories (like ETCS, SEAR and most likely the "typed set theories" mentioned in OP) is rather fundamental. To the point that calling both of them "set theory" feels quite misleading.

Maybe because there are many different set theories. The one taught in school is not a correct one but grokable for most students. Then you got the Zermeno Frenkel set theory, and you got the Homotopy Type Theory one which can yield or emulate the same results. So in a sense the opening statement is correct. There is no consensus on a single "this is THE one and true correct set theory"

what… argument? anyway, pretty sure larry is quite fluent with how mathematics is done.