| >OK, I'm being a little coy here, but to be completely serious, I think it's already a confusing enough topic and a bunch of pointless debates could be avoided with better terminology. Sure, I just don't think it's going to happen. The HoTT (and category theory) people largely don't care about (1), so they typically don't need to differentiate. More cynically, it's probably also just better marketing, a new 'foundation' certainly sounds more impressive than just a new 'mathematical framework', especially because (1) is generally pretty esoteric. >This can't be sense (2), because it refers to "unformalized mathematics." So it has to be sense (1). I don't think so, look at how they actually define 'unformalized mathematics': "Indeed, many of the proofs described in this book were actually first done in a fully formalized form in a proof assistant, and are only now being “unformalized” for the first time — a reversal of the usual relation between formal and informal mathematics." The idea is essentially that using HoTT formalisms informally can lead to new insight, which is exactly what part 2 of the book focuses on and they're making it clear that it's about general mathematics rather than metamathematics. If they were talking about (1), you'd expect them to at least do some actual metamathematics with it! I think your next sentence actually serves to support this further. >And this is not the only sentence of this kind, e.g., 'This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics.' And now consider how the sentence actually ends "- and convenient machine implementations, which can serve as a practical aid to the working mathematician". You could argue that it being a practical aid only refers to the convenient machine implementations, but how would 'homootopical content' or 'an "invariant" conception' remotely help with (1)? To me this makes it pretty clear that the aim is to have a practical 'foundation' for the average working mathematician i.e. (2). >So whatever you want to call it, this research is not really justifiable on traditional metamathematical grounds. The actual point seems to be facilitating the construction of proof assistants. Sure, that I don't disagree with, it's definitely in the area of 'applied metamathematics' and there's a reason type theory field is more on the CS side. I just think that you would generally get some pretty strange looks if you called e.g. research on sequent calculus an 'engineering problem', even though it's typically done with the intent of eventually getting a practical system. >I'm not sure what "there hasn't been any significant news for non-mathematicians" means here. For example, Quanta articles on various mathematical discoveries and sociological phenomena (from chalk to disagreements over the foundations of symplectic topology) routinely get posted on HN and are well received. If this is the bar for "significant for a non-mathematician," then I think finally formalizing a good chunk of "fashionable" mathematics is absolutely newsworthy My point is that often there has been no 'visible' (for a non-mathematician) progress made, so it's curious to me that despite this it still gets posted here every few months. I would have expected some attention if some larger milestone was reached (e.g. formalizing most of an undergrad degree), it's the consistency that is surprising to me. |
I read the introduction to the HoTT book again and it seems to clear to me the justifications offered there go well beyond just better proof assistants. ("Homotopy type theory also brings new ideas into the very foundation of mathematics.") This is also my experience reading HoTT-adjacent people on Twitter (John Baez, random grad students). They clearly have some, I don't know how to put this, fundamentally aesthetic concerns with set theory, and offer various arguments like the ones we agreed were bad.
I appreciate you pointing out that it is possible to make a totally reasonable case for HoTT as a research program that does not resort to such arguments. So I am left wondering why so many other people fail to do this.