5 ms·

It is great that someone with a Fields medal is interested in interactive theorem proving. And he is right that mathematics will completely change because of it

It is great that someone with a Fields medal is interested in interactive theorem proving. And he is right that mathematics will completely change because of it. Soon. I doubt though that HoTT is the way this revolutionary change will happen. If you don't believe me, try reading the first few pages of chapter 2 of the HoTT book. It is basically total gibberish to me, and yes, this is because I am neither well versed in constructive type theory, nor in homotopy theory. I DO have though 10+ years of experience in interactive theorem proving, as well have a diploma in math where I learnt the basic notions of topology. Now, if this is gibberish to me, it will be gibberish to about 99% of all mathematicians out there . A revolution does not happen by excluding 99% of its targeted population. HoTT will have to evolve into something much easier to understand with a clear value proposition to non-homotopy / non-type-theorists before I would even remotely consider it for providing the underpinnings of a system for interactive proof.

fedvasu 13y ago
what a load of bullshit. you don't even have a phD in mathematics, let alone in similar subject of HoTT. News flash calculus was considered very advanced curriculum for even mathematicians in 17th century, only discussed in scholarly correspondence of elite mathematicians and physicists. your ignorance is not the reason HoTT will fail/pass. This is not a programming language where the uptake depends on the stupidity of programmers. It is mathematical theory if the premise and potential is interesting enough it will thrive or perish. you are not special you are not a unique snowflake (neither am I). Science(mathematics is described as queen of sciences) needs good education to understand and appreciate it, you can't criticize which you don't understand. I would love to read informed criticism, I for one even welcome a little ridicule if it is justified by sound arguments.
- auggierose 13y ago
  But yes, this is (partly) a programming language where the uptake will depend on how easy it is to understand. By the way, I don't have a PhD in mathematics, but I do have a PhD in interactive theorem proving.
  - fedvasu 13y ago
    my point still stands, it is advanced mathematics at this stage. you do have a CS doctorate but as I said it requires time and refinement to make it accessible even for CS researchers. It is un-scientific to criticize and snub which you can't make informed arguments about.
- yoran 13y ago
  Would anyone mind clarifying what "HoTT" stands for?
  - shpx 13y ago
    http://lmgtfy.com/?q=HoTT http://lmgtfy.com/?q=HoTT read the article. HOmotopy Type Theory
  - ehsanu1 13y ago
    http://homotopytypetheory.org/ http://homotopytypetheory.org/
chas 13y ago
I am not a mathematician and I can't speak to the likelihood of a mathematical revolution, but as a programmer with interest in theoretical computer science and I found the HoTT book to be extremely useful. Prior to last year there were very few available and approachable resources for learning HoTT. Papers on the subject were hard to find and harder to understand for someone not in the field. Because of this, any textbook is a huge step forward for me even if it doesn't have mass appeal because it allows people who aren't directly researching HoTT to become familiar with the ideas and results and find further references to previous work. These people in turn can educate others who might be computationally or mathematically inclined and interested in the benefits of HoTT such as better interactive theorem proving, but don't have specific interest in type theory, category theory, or homotopy theory and therefore find existing resources difficult to understand.
deleted 13y ago
[deleted]
nilkn 13y ago
> it will be gibberish to about 99% of all mathematicians out there . If you'd said "programmer" instead of "mathematician," I'd agree with you. As it stands, though, those pages are reviewing just basic algebraic topology, which any practicing professional mathematician would know to some degree. These days, it's taught to top undergraduates and almost universally to first-year graduate students; it is also typically prominent material on PhD qualifying exams in mathematics.
ek 13y ago
Your criticism of the book does not appear to be constructive, meaningful, or well-founded. Rather than saying "this sux, wow" and then listing your credentials, it might help if you gave some idea of what complaints you actually have with the work. While calling someone else's work "gibberish" is a low enough blow that I'm not sure it warrants further discussion, I want to at least make a couple of specific points on what you have said: 1. Despite your claim that you are not versed in type theory, chapter 1 provides what I find, as a 21 year old graduate student in programming languages with a relatively standard undergraduate background in mathematics and then some, to be a clear and helpful explanation of Martin-Löf type theory, and a good exposition of background needed for chapter 2. Did you read it? 2. This book makes extremely clear that the "homotopy theory" that is developed towards the exposition of homotopy type theory is merely synthetic, which is to say that it considers homotopies as first class objects, rather than deriving them from their traditional topological underpinnings in a more analytic way. It might be useful to have a little understanding of point-set topology with maybe a little inkling of what's going on in algebraic topology to figure this out, but certainly it doesn't seem absolutely necessary, since the book's notion of homotopy is built from first principles. Are there specific points in chapter 2 that you find confusing? 3. It appears you have a doctorate in CS, specifically to do with interactive theorem proving. Almost every proof assistant I have come across either uses dependent types or higher-order logic, and it seems like in order to have earned a PhD in interactive theorem proving you might have had to have become familiar with at least one of these formalisms. Given that you should be comfortable in one of these domains, it doesn't seem like the material in the book is a huge leap. Could you speak a little bit more to what you worked on grad school? I don't mean to come across as harsh, but your claim that this book excludes 99% of its target population seems false; at the very least I do not consider myself in the top 1% of people who might hope to consume this book.
- auggierose 13y ago
  I did not call it gibberish. I said it was gibberish TO ME. Which is a big difference. Chapter 2 lost me at the point where infinity-groupoids entered the game. Until then everything was easy to understand. From then on I would have to seriously sit down and work with the book. With regard to constructive criticism: I told you what I want, make it easier to understand, and tell me what the value is for me (a non-constructive classical applied mathematician / programmer / engineer). Yep, I did not tell you HOW to get there. I see how that can be annoying for a constructive mathematician. So, maybe you can tell me: Why should I care about the univalence axiom as a non-constructivist ?
pavelrub 13y ago
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
judk 13y ago
You are a computer scientist, not a mathematician. This book is for mathematicians. (Not an insult, the mathematicians deep into homotopy aren't likely to be great at building an actual theorem prover on a computer.) Basic notions of topology only touch a bit of the corners of HoTT. Have you seen the Agda code on the HoTT github site? That might be closer to your language. Or poke around at Andrej Bauer's work, as he leans toward the computerization side a bit.
- auggierose 13y ago
  Lol. Fortunately, after finishing my "prediploma" in mathematics as the best of my university, I also realised that I am not going to be a mathematician, at least not in the sense that most people understand it then and now.

fedvasu 13y ago

what a load of bullshit. you don't even have a phD in mathematics, let alone in similar subject of HoTT. News flash calculus was considered very advanced curriculum for even mathematicians in 17th century, only discussed in scholarly correspondence of elite mathematicians and physicists. your ignorance is not the reason HoTT will fail/pass. This is not a programming language where the uptake depends on the stupidity of programmers. It is mathematical theory if the premise and potential is interesting enough it will thrive or perish. you are not special you are not a unique snowflake (neither am I). Science(mathematics is described as queen of sciences) needs good education to understand and appreciate it, you can't criticize which you don't understand. I would love to read informed criticism, I for one even welcome a little ridicule if it is justified by sound arguments.

auggierose 13y ago
But yes, this is (partly) a programming language where the uptake will depend on how easy it is to understand. By the way, I don't have a PhD in mathematics, but I do have a PhD in interactive theorem proving.
- fedvasu 13y ago
  my point still stands, it is advanced mathematics at this stage. you do have a CS doctorate but as I said it requires time and refinement to make it accessible even for CS researchers. It is un-scientific to criticize and snub which you can't make informed arguments about.
yoran 13y ago
Would anyone mind clarifying what "HoTT" stands for?
- shpx 13y ago
  http://lmgtfy.com/?q=HoTT http://lmgtfy.com/?q=HoTT read the article. HOmotopy Type Theory
- ehsanu1 13y ago
  http://homotopytypetheory.org/ http://homotopytypetheory.org/

chas 13y ago

I am not a mathematician and I can't speak to the likelihood of a mathematical revolution, but as a programmer with interest in theoretical computer science and I found the HoTT book to be extremely useful. Prior to last year there were very few available and approachable resources for learning HoTT. Papers on the subject were hard to find and harder to understand for someone not in the field. Because of this, any textbook is a huge step forward for me even if it doesn't have mass appeal because it allows people who aren't directly researching HoTT to become familiar with the ideas and results and find further references to previous work. These people in turn can educate others who might be computationally or mathematically inclined and interested in the benefits of HoTT such as better interactive theorem proving, but don't have specific interest in type theory, category theory, or homotopy theory and therefore find existing resources difficult to understand.

deleted 13y ago

[deleted]

nilkn 13y ago

> it will be gibberish to about 99% of all mathematicians out there . If you'd said "programmer" instead of "mathematician," I'd agree with you. As it stands, though, those pages are reviewing just basic algebraic topology, which any practicing professional mathematician would know to some degree. These days, it's taught to top undergraduates and almost universally to first-year graduate students; it is also typically prominent material on PhD qualifying exams in mathematics.

ek 13y ago

Your criticism of the book does not appear to be constructive, meaningful, or well-founded. Rather than saying "this sux, wow" and then listing your credentials, it might help if you gave some idea of what complaints you actually have with the work. While calling someone else's work "gibberish" is a low enough blow that I'm not sure it warrants further discussion, I want to at least make a couple of specific points on what you have said: 1. Despite your claim that you are not versed in type theory, chapter 1 provides what I find, as a 21 year old graduate student in programming languages with a relatively standard undergraduate background in mathematics and then some, to be a clear and helpful explanation of Martin-Löf type theory, and a good exposition of background needed for chapter 2. Did you read it? 2. This book makes extremely clear that the "homotopy theory" that is developed towards the exposition of homotopy type theory is merely synthetic, which is to say that it considers homotopies as first class objects, rather than deriving them from their traditional topological underpinnings in a more analytic way. It might be useful to have a little understanding of point-set topology with maybe a little inkling of what's going on in algebraic topology to figure this out, but certainly it doesn't seem absolutely necessary, since the book's notion of homotopy is built from first principles. Are there specific points in chapter 2 that you find confusing? 3. It appears you have a doctorate in CS, specifically to do with interactive theorem proving. Almost every proof assistant I have come across either uses dependent types or higher-order logic, and it seems like in order to have earned a PhD in interactive theorem proving you might have had to have become familiar with at least one of these formalisms. Given that you should be comfortable in one of these domains, it doesn't seem like the material in the book is a huge leap. Could you speak a little bit more to what you worked on grad school? I don't mean to come across as harsh, but your claim that this book excludes 99% of its target population seems false; at the very least I do not consider myself in the top 1% of people who might hope to consume this book.

auggierose 13y ago
I did not call it gibberish. I said it was gibberish TO ME. Which is a big difference. Chapter 2 lost me at the point where infinity-groupoids entered the game. Until then everything was easy to understand. From then on I would have to seriously sit down and work with the book. With regard to constructive criticism: I told you what I want, make it easier to understand, and tell me what the value is for me (a non-constructive classical applied mathematician / programmer / engineer). Yep, I did not tell you HOW to get there. I see how that can be annoying for a constructive mathematician. So, maybe you can tell me: Why should I care about the univalence axiom as a non-constructivist ?

pavelrub 13y ago

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

judk 13y ago

You are a computer scientist, not a mathematician. This book is for mathematicians. (Not an insult, the mathematicians deep into homotopy aren't likely to be great at building an actual theorem prover on a computer.) Basic notions of topology only touch a bit of the corners of HoTT. Have you seen the Agda code on the HoTT github site? That might be closer to your language. Or poke around at Andrej Bauer's work, as he leans toward the computerization side a bit.

auggierose 13y ago
Lol. Fortunately, after finishing my "prediploma" in mathematics as the best of my university, I also realised that I am not going to be a mathematician, at least not in the sense that most people understand it then and now.