Voevodsky’s Mathematical Revolution

http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/

by juliangamble • 13 years ago

145 76 13 years ago

blogs.scientificamerican.com

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• 13 years 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...

yetanotherphd3• 13 years 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.

nilkn2• 13 years 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...

ivan_ah• 13 years 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

Tyr42• 13 years 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_• 13 years ago

Wow, this is a very well written and readable book.

juliangamble3• 13 years 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-re...

ek8• 13 years ago

Thanks! I tried to answer it.

continuations• 13 years 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• 13 years ago

It is not automated theorem proving, but computer verified proving

ek8• 13 years 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• 13 years ago

I was under the impression that even verification is Turing undecidable in general - ie http://en.wikipedia.org/wiki/Entscheidungsproblem

joe_the_user2• 13 years 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

Chattered3• 13 years ago

It's standard to use a verifier to check the correctness of a computer program, by encoding the program and then doing proofs about it. As per Goedel, a verifier can't check the correctness of its own program. So they'll always be incomplete there.

Missing such a theorem isn't exactly a deal-breaker though.

ChristianMarks• 13 years 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• 13 years 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...

auggierose15• 13 years 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.

fedvasu2• 13 years 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.

auggierose15• 13 years 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.

yoran• 13 years ago

Would anyone mind clarifying what "HoTT" stands for?

chas2• 13 years 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.

nilkn2• 13 years 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.

ek8• 13 years 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.

auggierose15• 13 years 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 ?

pavelrub2• 13 years 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.

auggierose15• 13 years 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.

auggierose15• 13 years 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.

judk• 13 years 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.

auggierose15• 13 years 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.

DonGateley• 13 years 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.

juliangamble3• 13 years 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

They were presented at fpsyd.

juliangamble3• 13 years 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

stefantalpalaru• 13 years 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• 13 years 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/200269.html

tunesmith• 13 years 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?

chas2• 13 years 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

nardi• 13 years 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• 13 years 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?

solomatov2• 13 years 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/in...

And its based on on-line book Software Foundations http://www.cis.upenn.edu/~bcpierce/sf/toc.html which is really accessible for about anyone with small programming experience.

Voevodsky’s Mathematical Revolution

Related Stories