6 ms·

I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time. There are many intelligent and curious people re

I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time. There are many intelligent and curious people reading HN, who might be tempted to spend time understanding it because its somewhat frequent appearance here gives the (false) impression that it plays some important role in modern mathematics. I regret spending the (large) amount of time I did learning what it is about, only to realize that's not much actual content there, and I would hope my post saves other people that trouble. There is a lot of far more interesting, elegant, and useful mathematics out there, imo.

oisdk 6y ago
> I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time. This is a bizarre thing to say. Learning any mathematics is a complete waste of time. > gives the (false) impression that it plays some important role in modern mathematics. What are you talking about? HoTT is broadly regarded as an exciting and important new area of mathematics; your view is absolutely the minority view. I mean I don't think I'm going to be able to convince you otherwise if you genuinely think that there's "not much content" in HoTT, but there are loads of well-regarded and prominent mathematicians who hold the opposite view to yours.
- spekcular 6y ago
  Learning mathematics had been incredibly useful to me. If that hasn't been the case for you, I'm sorry. Your claim that HoTT is "broadly regarded as an exciting and important new area of mathematics" is simply wrong. I suggest talking to a wider variety of mathematicians. In particular, concerning "well-regarded and prominent mathematicians," Steve Simpson and Harvey Friedman are on record on the Foundations of Mathematics mailing list saying, essentially, that HoTT is a waste of time [0]. The other set theory experts I know agree with them but haven't said so publicly. My impression is that this is a fairly common view in the set theory and foundations community. Further, Jacob Lurie, who is perhaps the most talented mathematician currently working in higher category theory, has also written he doesn't think highly of it [1]. [0] I can provide links if it you want, but if you search the archive these arguments are easy to find. [1] View the comments on this blog post: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/13...
  - oisdk 6y ago
    > Learning mathematics had been incredibly useful to me. You have missed my point. We generally don't study only the "useful" things; if we did most of the most important mathematics we have today would have gone unstudied. > Your claim that HoTT is "broadly regarded as an exciting and important new area of mathematics" is simply wrong. According to whom? You? You're making an argument about consensus regarding the importance of a given area, but I have seen nothing to indicate that the consensus among mathematicians is in line with your opinion. > Steve Simpson and Harvey Friedman They are in the minority. Again, if you're arguing about consensus you can't just point to one or two individuals and say "look! They agree with me!" For goodness' sake, the thread your referring to is well-known partially because it was controversial. > Jacob Lurie [...] doesn't think highly of it The content of Lurie's comment and yours are quite different.
    - spekcular 6y ago
      You wrote that "Learning any mathematics is a complete waste of time." There are a variety of ways math could not be a waste of time; practical applications are only one. I don't mean to imply pure mathematics shouldn't be studied, only that I don't believe math was a time waster for me. > According to whom? I've talked to a lot of very good mathematicians, including people who've studied and collaborated with people in the HoTT orbit, and people from many other subfields. I'm sorry I don't have exact quantitative data for you. > They are in the minority. Again, if you're arguing about consensus you can't just point to one or two individuals and say "look! They agree with me!" For goodness' sake, the thread your referring to is well-known partially because it was controversial. Again, I don't think they're in the minority. Also, there's way more than one relevant thread. That particular fight was litigated over years. > The content of Lurie's comment and yours are quite different. He makes many comments on that post. I invite you to read them all. Certainly, I'm not just regurgitating what he says there, but it does provide an example of a top mathematician expressing skepticism about the entire enterprise.
      - oisdk 6y ago
        > You wrote that "Learning any mathematics is a complete waste of time." Yes, I was being facetious. My point is that by whatever measure pure maths is worth studying (i.e. those measure beyond "practical" applications) also obviously applies to HoTT. > I've talked to a lot of very good mathematicians You're an anonymous person on the internet, this is such a strange thing to fall back on. There are pretty standard ways of talking about how well-regarded/important certain subfields are in mathematics, "I've asked around" isn't one of them. > I'm not just regurgitating what he says there His comments express a substantially different point to yours. He does not say that HoTT is a waste of time, or that it "doesn't have much content".
pchiusano 6y ago
People find it interesting and fun so IMO that’s the only bar that needs to be cleared to justify the attention it gets. If your pet areas of mathematics are more exciting to you, then share that with people and/or post here and maybe it will get more attention. Or not! I wouldn’t dissuade people from following their interests. My background - I’m a programmer and like building programming languages. I’m interested in HoTT because I’m interested in type theory generally and also formalization of mathematics. Most mathematicians don’t care much about these things, which is fine. Like most weird stuff, it’s good that some folks are doing it. Lastly you might enjoy this thread about why formalization is interesting to another mathematician: https://mobile.twitter.com/andrejbauer?prefetchtimestamp=1603845667275 https://mobile.twitter.com/andrejbauer?prefetchtimestamp=160...
- spekcular 6y ago
  Your link does not work for me. Maybe there's a bug with Twitter, or my browser is blocking too many trackers? I want to clarify that I think formalizing mathematics is interesting, too! It's just entirely unclear to me that HoTT has any special advantages here (see link from my original post).
  - pchiusano 6y ago
    Here’s a link that works I think: https://mobile.twitter.com/andrejbauer/status/1259901971991052290 https://mobile.twitter.com/andrejbauer/status/12599019719910... The supposed selling point of HoTT wrt to formalizing mathematics is higher level proofs that are more general and are less work to express, due to having this richer notion of equivalence in the type theory. I think the post you linked is pretty good... it makes me wonder - at this point, what is holding back more formalization? Is it a cultural thing? (None of the people who are doing “interesting” math care about formalizing It) Is it a technical thing? (Proof assistants and their type theories aren’t good enough?) Are we just missing a big enough “standard library” of mathematics so mathematicians can get to the interesting parts sooner? It’s probably all of the above. What I think might happen is it reaches a tipping point where enough of the pieces are in place to where it rapidly becomes normal or expected to formalize mathematics and we have awesome tools and “standard libraries” to make it good.
Ericson2314 6y ago
Your comments indicate you do not understand it very well. I therefore also hope you didn't waste much time reading your current level of understanding.

oisdk 6y ago

> I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time. This is a bizarre thing to say. Learning any mathematics is a complete waste of time. > gives the (false) impression that it plays some important role in modern mathematics. What are you talking about? HoTT is broadly regarded as an exciting and important new area of mathematics; your view is absolutely the minority view. I mean I don't think I'm going to be able to convince you otherwise if you genuinely think that there's "not much content" in HoTT, but there are loads of well-regarded and prominent mathematicians who hold the opposite view to yours.

spekcular 6y ago
Learning mathematics had been incredibly useful to me. If that hasn't been the case for you, I'm sorry. Your claim that HoTT is "broadly regarded as an exciting and important new area of mathematics" is simply wrong. I suggest talking to a wider variety of mathematicians. In particular, concerning "well-regarded and prominent mathematicians," Steve Simpson and Harvey Friedman are on record on the Foundations of Mathematics mailing list saying, essentially, that HoTT is a waste of time [0]. The other set theory experts I know agree with them but haven't said so publicly. My impression is that this is a fairly common view in the set theory and foundations community. Further, Jacob Lurie, who is perhaps the most talented mathematician currently working in higher category theory, has also written he doesn't think highly of it [1]. [0] I can provide links if it you want, but if you search the archive these arguments are easy to find. [1] View the comments on this blog post: https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ https://mathematicswithoutapologies.wordpress.com/2015/05/13...
- oisdk 6y ago
  > Learning mathematics had been incredibly useful to me. You have missed my point. We generally don't study only the "useful" things; if we did most of the most important mathematics we have today would have gone unstudied. > Your claim that HoTT is "broadly regarded as an exciting and important new area of mathematics" is simply wrong. According to whom? You? You're making an argument about consensus regarding the importance of a given area, but I have seen nothing to indicate that the consensus among mathematicians is in line with your opinion. > Steve Simpson and Harvey Friedman They are in the minority. Again, if you're arguing about consensus you can't just point to one or two individuals and say "look! They agree with me!" For goodness' sake, the thread your referring to is well-known partially because it was controversial. > Jacob Lurie [...] doesn't think highly of it The content of Lurie's comment and yours are quite different.
  - spekcular 6y ago
    You wrote that "Learning any mathematics is a complete waste of time." There are a variety of ways math could not be a waste of time; practical applications are only one. I don't mean to imply pure mathematics shouldn't be studied, only that I don't believe math was a time waster for me. > According to whom? I've talked to a lot of very good mathematicians, including people who've studied and collaborated with people in the HoTT orbit, and people from many other subfields. I'm sorry I don't have exact quantitative data for you. > They are in the minority. Again, if you're arguing about consensus you can't just point to one or two individuals and say "look! They agree with me!" For goodness' sake, the thread your referring to is well-known partially because it was controversial. Again, I don't think they're in the minority. Also, there's way more than one relevant thread. That particular fight was litigated over years. > The content of Lurie's comment and yours are quite different. He makes many comments on that post. I invite you to read them all. Certainly, I'm not just regurgitating what he says there, but it does provide an example of a top mathematician expressing skepticism about the entire enterprise.
    - oisdk 6y ago
      > You wrote that "Learning any mathematics is a complete waste of time." Yes, I was being facetious. My point is that by whatever measure pure maths is worth studying (i.e. those measure beyond "practical" applications) also obviously applies to HoTT. > I've talked to a lot of very good mathematicians You're an anonymous person on the internet, this is such a strange thing to fall back on. There are pretty standard ways of talking about how well-regarded/important certain subfields are in mathematics, "I've asked around" isn't one of them. > I'm not just regurgitating what he says there His comments express a substantially different point to yours. He does not say that HoTT is a waste of time, or that it "doesn't have much content".

pchiusano 6y ago

People find it interesting and fun so IMO that’s the only bar that needs to be cleared to justify the attention it gets. If your pet areas of mathematics are more exciting to you, then share that with people and/or post here and maybe it will get more attention. Or not! I wouldn’t dissuade people from following their interests. My background - I’m a programmer and like building programming languages. I’m interested in HoTT because I’m interested in type theory generally and also formalization of mathematics. Most mathematicians don’t care much about these things, which is fine. Like most weird stuff, it’s good that some folks are doing it. Lastly you might enjoy this thread about why formalization is interesting to another mathematician: https://mobile.twitter.com/andrejbauer?prefetchtimestamp=1603845667275 https://mobile.twitter.com/andrejbauer?prefetchtimestamp=160...

spekcular 6y ago
Your link does not work for me. Maybe there's a bug with Twitter, or my browser is blocking too many trackers? I want to clarify that I think formalizing mathematics is interesting, too! It's just entirely unclear to me that HoTT has any special advantages here (see link from my original post).
- pchiusano 6y ago
  Here’s a link that works I think: https://mobile.twitter.com/andrejbauer/status/1259901971991052290 https://mobile.twitter.com/andrejbauer/status/12599019719910... The supposed selling point of HoTT wrt to formalizing mathematics is higher level proofs that are more general and are less work to express, due to having this richer notion of equivalence in the type theory. I think the post you linked is pretty good... it makes me wonder - at this point, what is holding back more formalization? Is it a cultural thing? (None of the people who are doing “interesting” math care about formalizing It) Is it a technical thing? (Proof assistants and their type theories aren’t good enough?) Are we just missing a big enough “standard library” of mathematics so mathematicians can get to the interesting parts sooner? It’s probably all of the above. What I think might happen is it reaches a tipping point where enough of the pieces are in place to where it rapidly becomes normal or expected to formalize mathematics and we have awesome tools and “standard libraries” to make it good.

Ericson2314 6y ago

Your comments indicate you do not understand it very well. I therefore also hope you didn't waste much time reading your current level of understanding.