This kind of foundational (ZFC,CT,HTT) stuff is pretty niche in mathematics.
Set theory, though touted as the foundation of math, isn't really used to its full extremes (HOD, etc) by anyone but set theorists. Its more like... A common datatype?
And while CT could also be a foundation, as far as im aware its only practical uses as a tool are found in commutative algebra.
I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.
> I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.
I agree -- most fields of math are happy to establish their own axioms, and leave the reducibility of those axioms to some "foundations" as an exercise -- an important one, but not one that necessarily furthers the field itself.
However, Voevodsky's stated aim for his Univalent Foundations project was not to formalize everything under a grand theory of everything. He got the bejeebus scared out of him when one of his results was very, very subtly wrong, in a way that was difficult for mathematicians to verify for years, even given a reasonable inkling of a counterexample. So he sought to improve the state of the art in proof verification.
You might argue, it's better to produce a verification tool for one field of mathematics than all of them at once. But you'll have a hard time finding any significantly complex theorem that doesn't draw insight from multiple places. (Arguably, that's why they're significantly complex in the first place). And all fields of mathematics have some basic elements in common. So, I'd argue, you're unlikely to do a good job for any but the most narrow domains of mathematics without seeking some level of generality.
Any "foundation of mathematics" can be used for this purpose, and plenty of theorem provers have been built on each (Twelf, PVS, Agda). The draw of category theory is that it seems to capture at a fundamental level many of the basic conceptual elements we see across mathematics. (Homomorphisms are so universal it's not even funny.) It seems reasonable to pick something that starts us closer to where we want to be; the difficulties we encounter are more likely to be fundamental problems and not issues of encoding.
Couldn’t agree more. I am a current (mid career) PhD student in cryptography and WOW is it a mess. Provable security arguments are generally written in the implicit propositional logic + set theory of working mathematicians, but it is woefully inadequate for the job. Some very powerful composable frameworks have been developed, but they are really straining against the clunkiness of the formal system in which they have been constructed. The best new ideas I’ve seen for formalizing cryptographic settings all belong in category theory or topology, but have been formalized in set theory because that seems to be the only tool that the average cryptographer intuitively knows how to use.
Im not opposed to the use of proof assistant software for difficult theorems.
And if one foundation or another is more applicable to that software, then thats fine.
Its more the narrative of the grand unification of mathematics thats spun around 'foundational theories' that irks me. In reality its just various emulation schemes.
Rephrasing other mathematicians work and claiming fundamental status, while not producing many novel theorems... just strikes me as very distasteful.
I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.