I have no objections to claiming success in formalizing mathematics! As I've said, Lean is a big win for type theory.
But formalizing proofs with computers is essentially separate from the rigorous study of the foundations of math (consistency, relative strength of theories, etc.).
You've complained above about set theorists not learning "your stuff," and now it's my turn to complain. You write: 'Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care).' Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations.
And yeah, I'm aware the HoTT people have ways around this, fine. My comment is more about the perspective conveyed by your remarks: if you want to have a seat at the table in a discussion about foundational issues, you need to understand basic facts like this. My suspicion is that you might have had bad interactions with set theorists because you don't share certain knowledge they take for granted, and then they get frustrated and end the conversation early. I truly believe that if you went and read a book on set theory and logic, and learned, e.g., wny large cardinals are important, you might understand better where I and other people are coming from.
> Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations.
It's my understanding that some larger cardinals are needed for foundations, but since the foundations problem was "solved" future work on large cardinals has continued, and that is more "more set theory for set theory's sake", than something needed to accommodate math other "regular" mathematicians are doing.
(With the possible exception of the Grothendiek and Voevodsky line of problems perhaps as the article relates --- separate and ancillary to Voevodsky's desire for a proof checker, and also separate to whether or not categorical methods alone can suffice.)
I actually don't know of type theory having "ways around this". My understanding is that while type theory doesn't appear to face fundamental obstacles here, set theory "has the lead" in making large cardinals (or their equivalents) due to being older, and the type theorists relative disinterest in this area has meant the gap is not closing.
Large cardinals are closely related to what type theorists call "universes". Again, there's a huge amount of equiconsistency and relative consistency results linking type- and set theories. To keep suggesting and implying that type theory cannot possibly be a language for talking about these things is so incredibly careless and obtuse that some people might call it actively misleading.
I'm not sure how that comment is responsive to my post. Sure, type theorists talk about universes, and sure, there are relative consistency results linking type and set theories. My claim is just that large cardinals (or some equivalent concept) are essentially necessary to order theories in consistency strength, so is hard to take a response of the form "it doesn't matter whether HoTT can talk about large cardinals" seriously.
But formalizing proofs with computers is essentially separate from the rigorous study of the foundations of math (consistency, relative strength of theories, etc.).
You've complained above about set theorists not learning "your stuff," and now it's my turn to complain. You write: 'Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care).' Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations.
And yeah, I'm aware the HoTT people have ways around this, fine. My comment is more about the perspective conveyed by your remarks: if you want to have a seat at the table in a discussion about foundational issues, you need to understand basic facts like this. My suspicion is that you might have had bad interactions with set theorists because you don't share certain knowledge they take for granted, and then they get frustrated and end the conversation early. I truly believe that if you went and read a book on set theory and logic, and learned, e.g., wny large cardinals are important, you might understand better where I and other people are coming from.