5 ms·

I do not understand your criticism. HoTT's value proposition is about a significant simplification of automated theorem proving in mathematics. As such, the val

I do not understand your criticism. HoTT's value proposition is about a significant simplification of automated theorem proving in mathematics. As such, the value proposition itself has nothing to do with Homotopy Theory: if what HoTT promises to deliver will indeed happen, mathematicians will learn the necessary material because of what it gives them. Perhaps you are saying that it simply won't deliver, but you cannot possibly reach such a conclusion by reading 1.5 chapters out of 11. I do not understand how the fact that currently most people do not know the relevant material is an argument against HoTT: of course nobody knows it: it's new! Did you expect "revolutions" to happen by telling people something they already know? Do you believe Grothendieck's work was a mistake because 99.9999% percent of mathematicians weren't Algebraic Geometers by the time EGA was published? Your argument makes no sense, maybe because you are comparing HoTT to Facebook, when in fact it's a mathematical achievement. Also: if this is gibberish to me, it will be gibberish to about 99% of all mathematicians out there . I seriously doubt that.

auggierose 13y ago
> HoTT's value proposition is about a significant simplification of automated theorem proving in mathematics. Now that is utter and complete nonsense. And that is why I am criticising HoTT. HoTT might be a beautiful mathematical theory. I am not competent in judging that, to be so, I would have to invest more time. But there is not a single shred of evidence that HoTT will improve automated, or for that matter interactive theorem proving. And I am pretty competent to judge that.
- pavelrub 13y ago
  I'm not sure what you are basing this on. How can you judge that if you do not understand the theory or the motivation behind it? Because chapter 2 seemed like gibberish to you? Read for example: http://homotopytypetheory.org/2013/03/08/homotopy-theory-in-homotopy-type-theory-introduction/ http://homotopytypetheory.org/2013/03/08/homotopy-theory-in-...
  - auggierose 13y ago
    I know that we are already very well capable of doing succinct proofs in interactive theorem proving systems like Isabelle that have a strong resemblance to "human" proofs. None of the proofs displayed in HoTT or the accompanying sources look shorter or more succinct than stuff I could do without HoTT. So HoTT might solve a problem for constructivists working with Coq. Problems you can entirely avoid by not working constructively (or with Coq, for that matter). Therefore, at this point, there is no evidence at all that HoTT might improve the state of the art in interactive theorem proving. That does not mean that this evidence might not come up at some point. How can I be sure in my judgement? Well, I don't have to understand string theory to be sure at this point that it is not relevant to interactive theorem proving. I would change my mind if somebody points out evidence that string theory is actually of major relevance to interactive theorem proving. Edit: I would even start learning string theory then.
auggierose 13y ago
For the 99% of all mathematicians statement: I should probably take that back, as I don't know what the curriculum for mathematicians looks like these days. Maybe it's all algebraic topology and category theory for them now. Instead of mathematician, I mean: people who could potentially benefit from interactive theorem proving technology.

auggierose 13y ago

> HoTT's value proposition is about a significant simplification of automated theorem proving in mathematics. Now that is utter and complete nonsense. And that is why I am criticising HoTT. HoTT might be a beautiful mathematical theory. I am not competent in judging that, to be so, I would have to invest more time. But there is not a single shred of evidence that HoTT will improve automated, or for that matter interactive theorem proving. And I am pretty competent to judge that.

pavelrub 13y ago
I'm not sure what you are basing this on. How can you judge that if you do not understand the theory or the motivation behind it? Because chapter 2 seemed like gibberish to you? Read for example: http://homotopytypetheory.org/2013/03/08/homotopy-theory-in-homotopy-type-theory-introduction/ http://homotopytypetheory.org/2013/03/08/homotopy-theory-in-...
- auggierose 13y ago
  I know that we are already very well capable of doing succinct proofs in interactive theorem proving systems like Isabelle that have a strong resemblance to "human" proofs. None of the proofs displayed in HoTT or the accompanying sources look shorter or more succinct than stuff I could do without HoTT. So HoTT might solve a problem for constructivists working with Coq. Problems you can entirely avoid by not working constructively (or with Coq, for that matter). Therefore, at this point, there is no evidence at all that HoTT might improve the state of the art in interactive theorem proving. That does not mean that this evidence might not come up at some point. How can I be sure in my judgement? Well, I don't have to understand string theory to be sure at this point that it is not relevant to interactive theorem proving. I would change my mind if somebody points out evidence that string theory is actually of major relevance to interactive theorem proving. Edit: I would even start learning string theory then.

auggierose 13y ago

For the 99% of all mathematicians statement: I should probably take that back, as I don't know what the curriculum for mathematicians looks like these days. Maybe it's all algebraic topology and category theory for them now. Instead of mathematician, I mean: people who could potentially benefit from interactive theorem proving technology.