I agree with you that this is really about the foundations of algebraic topology, but what makes you say that these are not the foundations of mathematics? In t

I agree with you that this is really about the foundations of algebraic topology, but what makes you say that these are not the foundations of mathematics? In the community of computer-aided formalization, a lot of interest in modern type theory arose, because some things in algebraic topology just couldn't easily be done in the old First-order-logic + ZFC framework: For example, Kevin Buzzard once asked if Isabelle/HOL (which even uses higher-order-logic) can even be used to formalize schemes! (It turns out that it is possible if you do it in a special way with locales... but the Lean formalization still seems more elegant). Of course, there is a consistency proof of Leans type theory using inaccessible cardinals, so the construction of schemes carries over to ZFC+large cardinals, but then it is not very understandable anymore. I agree with your point about HoTT not being useful to the algebraic topology community, but this seems orthogonal to its usefulness in formalization: I also would not expect Lean's type theory to be directly useful to working mathematicians. Instead it can make formalization easy or even possible: Even Jacob Lurie seems to acknowledge that it could be useful for that and only disputes that it does not bring new insights on an intuitive, informal level. My reading of the discussion is that some HoTT proponents see HoTT as a new language of mathematics (similar to category theory) and that Lurie does not believe that this perspective adds much, but that he does believe that one can use that perspective to understand the theorems. In the linked discussion Voevodsky points out that "Calculus of Inductive Constructions, the type theory that we currently using to formalize mathematics in the univalent style [and basically what Lean uses] is surprisingly convenient for doing mathematics at the level of sets and categories (and maybe 2-categories). As for mathematics of higher h-levels it is, in practice, of very little use. Note that this is a great advance of what was before as before we did not even have a system for doing abstract mathematics both formally and conveniently at the level of sets." [0] This highlights how crucial type theory is to do modern algebraic topology, even as he seems to claim that HoTT actually can not formalize Lurie's work? Still, he seems to agree that dependent type theories were a step in the right direction (unsurprisingly, since he founded HoTT) and that more work is needed for finding new foundations for mathematics. Indeed, the, as you write below, "mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century" is something that some people in foundations (and close to the Lean community) like Jeremy Avigad are actively pursuing: see e.g. https://arxiv.org/pdf/2009.09541.pdf https://arxiv.org/pdf/2009.09541.pdf [0]: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/comment-page-1/#comment-270 https://mathematicswithoutapologies.wordpress.com/2015/05/13...