4 ms·

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 mo

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.

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.