8 ms·

Voevodsky’s Mathematical Revolution

145 points by juliangamble 13y ago

yetanotherphd 13y ago
Everything the article says about the problems with set theory as foundations of mathematics rings true. I haven't had time to investigate homotopy type theory yet, but I hope that it lives up to the claims in the article.
- jonsterling 13y ago
  HoTT is really fun. I'm particularly interested to see if the computational behavior of univalent and higher inductive types gets sussed out (or else, like Bob Harper, I shall have to pick up my toys and head home). Computing with univalence and HITs sounds lovely, if only we could figure out how to do it...
  - yetanotherphd 13y ago
    What is a good way to get started with this literature? And is it better to read theory first, or read theory in conjunction with using languages like Haskell and Coq? I studied a lot of mathematics, and I find this fascinating, but I've found it hard to read the literature on type theory, and mathematical logic also.
    - ek 13y ago
      It seems like I end up plugging the book really frequently here, but it's for good reason -- it's exceptionally readable AND it's accompanied by a full Coq development. That is, you can do basically every exercise in the book, directly in Coq, if you want. You can definitely just read the material and then come back and try the exercises in Coq later, or more tightly couple the two. I think either approach would work well, and it's up to personal preference. The first chapter of HoTT is an introduction to Martin-Löf that I personally find quite intuitive, to the point that I'd say it's clear than most other expositions of the same material that I've tried to read. It will be easier to understand dependent type theory if you're programmed in a dependently typed language, but I wouldn't say it's strictly necessary to understand dependent types theoretically. I have just a little bit of Coq experience and found myself comfortable with the HoTT presentation of dependent types.
      - tel 13y ago
        I have only managed to get through the first chapter myself and I really want to reiterate that—the first chapter does a fantastic job presenting MLTT.
      - yetanotherphd 13y ago
        thanks for the pointers. I gave up with Martin-Löf type theory reading other texts, so I'm looking forward to trying again with this book.
    - RoboTeddy 13y ago
      I asked this question in ##hott on freenode last week, and someone recommended http://www.cs.cmu.edu/~rwh/courses/hott/ http://www.cs.cmu.edu/~rwh/courses/hott/
nilkn 13y ago
I'm quite familiar with homotopy theory but had never, prior to this point, taken a serious look at homotopy type theory. The following appears to be a great (highly technical) introduction: http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf http://hottheory.files.wordpress.com/2013/03/hott-online-323...
- ivan_ah 13y ago
  Interestingly, the entire source code of the HoTT book is available on github and it is under active development: https://github.com/HoTT/book https://github.com/HoTT/book
  - Tyr42 13y ago
    Which is a great boon, as I've edited the latex and recompiled it to fit perfectly on my Kindle. I really wish more people would open source their books.
- kitsune_ 13y ago
  Wow, this is a very well written and readable book.
juliangamble 13y ago
There is a question raised about the research outcomes of the event mentioned in the blog post here: http://cs.stackexchange.com/questions/19001/what-were-the-research-outcomes-of-the-univalent-foundations-program-year-homot http://cs.stackexchange.com/questions/19001/what-were-the-re...
- ek 13y ago
  Thanks! I tried to answer it.
  - deleted 13y ago
    [deleted]
continuations 13y ago
> Soon, they won’t consider a theorem proven until a computer has verified it. Is automated theorem proving really this close to being this powerful? So soon we'd be able to feed the proof of Poincare Conjecture to a computer and it'd be able to verify the proof? I was under the impression we were nowhere close to being able to do that.
- pirriperdos 13y ago
  It is not automated theorem proving, but computer verified proving
- ek 13y ago
  Technically Coq is not a fully automated automated prover, but leaving that aside: We are definitely not even close. But getting mathematicians acquainted with HoTT is a good first step, I think. The book itself presents formulations of homotopy theory, set theory, category theory, and a constructive view of the real numbers, all within homotopy type theory, and on top of all this we could likely start building up a corpus of more results from topology, algebra, and analysis.
- byerley 13y ago
  I was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.org/wiki/Entscheidungsproblem
  - joe_the_user 13y ago
    It's easy for impressions of undecidability to get out of hand. But actually, verification is computable. Verification has to be computable for things like Godel's theorem to work. If you read your link carefully, you'll notice it's about provability via axioms, not verification. Peace
    - jonahx 13y ago
      joe, what is the difference between verification and provability?
ChristianMarks 13y ago
Awodey and Voevodsky hit on connections between type theory and homotopy theory about the same time. It isn't clear how to find normal forms for dependent type theory with the univalence axiom added. Mathematicians of my acquaintance find curious the attraction of what appears to be another constructive type theory of interest primarily to (functional) programmers. To them it looks like a calculus for doing synthetic homotopy theory.
jackmaney 13y ago
I heard many of these claims--especially that there would soon be a Brave New World of Mathematics where proofs via computer would be the norm--about a decade ago, when I was in grad school. Let's just say that I'm not holding my breath...
auggierose 13y ago
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.
DonGateley 13y ago
I sure wish I could listen to his talk but the moron who recorded it wasn't looking at his meters or listening to a monitor. The clipping distortion is far beyond my ability to tolerate for more than about 10 seconds. Incredible incompetence.
- deleted 13y ago
  [deleted]
juliangamble 13y ago
There are some great slides by Liam O'Connor that draw the link between first-order logic and Martin-Löf type theory here: http://www.cse.unsw.edu.au/~liamoc/talk.pdf http://www.cse.unsw.edu.au/~liamoc/talk.pdf They were presented at fpsyd.
juliangamble 13y ago
If you're interested in Agda Proofs - this is a well written post by Brian McKenna demonstrating that the sum of two odd numbers is always even. http://brianmckenna.org/blog/plus_equals_even_take_2 http://brianmckenna.org/blog/plus_equals_even_take_2
stefantalpalaru 13y ago
>It turns out, however, that ArXiv isn’t yet up to the task — while it can accept attached files, they can’t have any directory structure. Why not archive and compress them in a tar.gz ?
menato 13y ago
There is some rather interesting interview with Vladimir (in russian), which shows a little of his underlying motivation: http://baaltii1.livejournal.com/198675.html http://baaltii1.livejournal.com/198675.html http://baaltii1.livejournal.com/200269.html http://baaltii1.livejournal.com/200269.html
tunesmith 13y ago
I got lost on one basic thing. I thought Coq wasn't based on HoTT. I thought Agda was based on Martin-Lof; Coq was based on calculus of constructions, and that would mean that the HoTT people are looking to develop a new proof assistant that is based on HoTT. Is that true?
- chas 13y ago
  Coq isn't based on HoTT, however, the people working on HoTT use a modified version of Coq in conjunction with a library that contains the essential elements. https://github.com/HoTT/HoTT https://github.com/HoTT/HoTT
  - nardi 13y ago
    The lightbulb moment for Voevodsky was apparently realizing that CoC (used in Coq) is almost entirely equivalent to HoTT. So in a sense, Coq actually is kind of based on HoTT, just using different words. (One could maybe say there is a homotopy between CoC and HoTT?? IANAM.) The library they are developing is basically a restatement of HoTT in Coq using more familiar terms/concepts.
aniijbod 13y ago
For and on behalf of any genuine non-mathematicians, a couple of questions: (1) what would have to be the case such that his latest advances in proof assistance would not live up to his expectations (2) what things outside the world of abstract mathematics (such as in, but not restricted to the world of software) would change (such that anyone outside the field would notice) if they did live up to his expectations?
solomatov 13y ago
Many people probably want to learn coq after reading the article and watching the video. Vladimir mentions that he had a course at Princeton where he learned Coq. Most probably this is the course: http://www.cs.princeton.edu/courses/archive/fall10/cos441/index.php http://www.cs.princeton.edu/courses/archive/fall10/cos441/in... And its based on on-line book Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/toc.html http://www.cis.upenn.edu/~bcpierce/sf/toc.html which is really accessible for about anyone with small programming experience.

145 points by juliangamble 13y ago

Everything the article says about the problems with set theory as foundations of mathematics rings true. I haven't had time to investigate homotopy type theory yet, but I hope that it lives up to the claims in the article.

jonsterling 13y ago
HoTT is really fun. I'm particularly interested to see if the computational behavior of univalent and higher inductive types gets sussed out (or else, like Bob Harper, I shall have to pick up my toys and head home). Computing with univalence and HITs sounds lovely, if only we could figure out how to do it...
- yetanotherphd 13y ago
  What is a good way to get started with this literature? And is it better to read theory first, or read theory in conjunction with using languages like Haskell and Coq? I studied a lot of mathematics, and I find this fascinating, but I've found it hard to read the literature on type theory, and mathematical logic also.
  - ek 13y ago
    It seems like I end up plugging the book really frequently here, but it's for good reason -- it's exceptionally readable AND it's accompanied by a full Coq development. That is, you can do basically every exercise in the book, directly in Coq, if you want. You can definitely just read the material and then come back and try the exercises in Coq later, or more tightly couple the two. I think either approach would work well, and it's up to personal preference. The first chapter of HoTT is an introduction to Martin-Löf that I personally find quite intuitive, to the point that I'd say it's clear than most other expositions of the same material that I've tried to read. It will be easier to understand dependent type theory if you're programmed in a dependently typed language, but I wouldn't say it's strictly necessary to understand dependent types theoretically. I have just a little bit of Coq experience and found myself comfortable with the HoTT presentation of dependent types.
    - tel 13y ago
      I have only managed to get through the first chapter myself and I really want to reiterate that—the first chapter does a fantastic job presenting MLTT.
    - yetanotherphd 13y ago
      thanks for the pointers. I gave up with Martin-Löf type theory reading other texts, so I'm looking forward to trying again with this book.
  - RoboTeddy 13y ago
    I asked this question in ##hott on freenode last week, and someone recommended http://www.cs.cmu.edu/~rwh/courses/hott/ http://www.cs.cmu.edu/~rwh/courses/hott/

nilkn 13y ago

I'm quite familiar with homotopy theory but had never, prior to this point, taken a serious look at homotopy type theory. The following appears to be a great (highly technical) introduction: http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf http://hottheory.files.wordpress.com/2013/03/hott-online-323...

ivan_ah 13y ago
Interestingly, the entire source code of the HoTT book is available on github and it is under active development: https://github.com/HoTT/book https://github.com/HoTT/book
- Tyr42 13y ago
  Which is a great boon, as I've edited the latex and recompiled it to fit perfectly on my Kindle. I really wish more people would open source their books.
kitsune_ 13y ago
Wow, this is a very well written and readable book.

juliangamble 13y ago

There is a question raised about the research outcomes of the event mentioned in the blog post here: http://cs.stackexchange.com/questions/19001/what-were-the-research-outcomes-of-the-univalent-foundations-program-year-homot http://cs.stackexchange.com/questions/19001/what-were-the-re...

ek 13y ago
Thanks! I tried to answer it.
- deleted 13y ago
  [deleted]

continuations 13y ago

> Soon, they won’t consider a theorem proven until a computer has verified it. Is automated theorem proving really this close to being this powerful? So soon we'd be able to feed the proof of Poincare Conjecture to a computer and it'd be able to verify the proof? I was under the impression we were nowhere close to being able to do that.

pirriperdos 13y ago
It is not automated theorem proving, but computer verified proving
ek 13y ago
Technically Coq is not a fully automated automated prover, but leaving that aside: We are definitely not even close. But getting mathematicians acquainted with HoTT is a good first step, I think. The book itself presents formulations of homotopy theory, set theory, category theory, and a constructive view of the real numbers, all within homotopy type theory, and on top of all this we could likely start building up a corpus of more results from topology, algebra, and analysis.
byerley 13y ago
I was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem http://en.wikipedia.org/wiki/Entscheidungsproblem
- joe_the_user 13y ago
  It's easy for impressions of undecidability to get out of hand. But actually, verification is computable. Verification has to be computable for things like Godel's theorem to work. If you read your link carefully, you'll notice it's about provability via axioms, not verification. Peace
  - jonahx 13y ago
    joe, what is the difference between verification and provability?

ChristianMarks 13y ago

Awodey and Voevodsky hit on connections between type theory and homotopy theory about the same time. It isn't clear how to find normal forms for dependent type theory with the univalence axiom added. Mathematicians of my acquaintance find curious the attraction of what appears to be another constructive type theory of interest primarily to (functional) programmers. To them it looks like a calculus for doing synthetic homotopy theory.

jackmaney 13y ago

I heard many of these claims--especially that there would soon be a Brave New World of Mathematics where proofs via computer would be the norm--about a decade ago, when I was in grad school. Let's just say that I'm not holding my breath...

auggierose 13y ago

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.

DonGateley 13y ago

I sure wish I could listen to his talk but the moron who recorded it wasn't looking at his meters or listening to a monitor. The clipping distortion is far beyond my ability to tolerate for more than about 10 seconds. Incredible incompetence.

deleted 13y ago
[deleted]

juliangamble 13y ago

There are some great slides by Liam O'Connor that draw the link between first-order logic and Martin-Löf type theory here: http://www.cse.unsw.edu.au/~liamoc/talk.pdf http://www.cse.unsw.edu.au/~liamoc/talk.pdf They were presented at fpsyd.

juliangamble 13y ago

If you're interested in Agda Proofs - this is a well written post by Brian McKenna demonstrating that the sum of two odd numbers is always even. http://brianmckenna.org/blog/plus_equals_even_take_2 http://brianmckenna.org/blog/plus_equals_even_take_2

stefantalpalaru 13y ago

>It turns out, however, that ArXiv isn’t yet up to the task — while it can accept attached files, they can’t have any directory structure. Why not archive and compress them in a tar.gz ?

menato 13y ago

There is some rather interesting interview with Vladimir (in russian), which shows a little of his underlying motivation: http://baaltii1.livejournal.com/198675.html http://baaltii1.livejournal.com/198675.html http://baaltii1.livejournal.com/200269.html http://baaltii1.livejournal.com/200269.html

tunesmith 13y ago

I got lost on one basic thing. I thought Coq wasn't based on HoTT. I thought Agda was based on Martin-Lof; Coq was based on calculus of constructions, and that would mean that the HoTT people are looking to develop a new proof assistant that is based on HoTT. Is that true?

chas 13y ago
Coq isn't based on HoTT, however, the people working on HoTT use a modified version of Coq in conjunction with a library that contains the essential elements. https://github.com/HoTT/HoTT https://github.com/HoTT/HoTT
- nardi 13y ago
  The lightbulb moment for Voevodsky was apparently realizing that CoC (used in Coq) is almost entirely equivalent to HoTT. So in a sense, Coq actually is kind of based on HoTT, just using different words. (One could maybe say there is a homotopy between CoC and HoTT?? IANAM.) The library they are developing is basically a restatement of HoTT in Coq using more familiar terms/concepts.

aniijbod 13y ago

For and on behalf of any genuine non-mathematicians, a couple of questions: (1) what would have to be the case such that his latest advances in proof assistance would not live up to his expectations (2) what things outside the world of abstract mathematics (such as in, but not restricted to the world of software) would change (such that anyone outside the field would notice) if they did live up to his expectations?

solomatov 13y ago

Many people probably want to learn coq after reading the article and watching the video. Vladimir mentions that he had a course at Princeton where he learned Coq. Most probably this is the course: http://www.cs.princeton.edu/courses/archive/fall10/cos441/index.php http://www.cs.princeton.edu/courses/archive/fall10/cos441/in... And its based on on-line book Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/toc.html http://www.cis.upenn.edu/~bcpierce/sf/toc.html which is really accessible for about anyone with small programming experience.