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.
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.
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 ?
To be clear, constructive mathematics are new to me as well. The section in the introduction titled "Constructivity" may help you -- it is about trying to come to grips with the constructive nature of type theory. The short answer is that much of the mathematics that we might want to do does not require the law of the excluded middle or the axiom of choice at all when approached from a type-theoretic point of view. Higher inductive types eliminate the reliance classical logic will frequently have on either of these. To quote an example from this section, "In set-theoretic foundations, the statement 'every fully faithful and essentially surjective functor is an equivalence of categories' is equivalent to the axiom of choice. But with the univalence axiom, it is just true; see Chapter 9."
The emphasis that you are placing on the fact that type theory happens to be a constructive logic is perhaps causing you to miss the point. Homotopy type theory is not about advocating constructivism. The "big idea" is that HoTT is a foundation that computers can already reason about easily, based on the work that has already been invested into developing sufficiently powerful dependently typed languages (Coq, Agda). Because it is possible to formulate set theory, category theory, and even real numbers (all discussed in part 2 of the book) within the framework of homotopy type theory, it should be possible to extend these formulations to encompass more and more results from the rest of the mathematics. Because HoTT has already been shown to be implementable (in the form of a library for Coq), this means that any math that is done informally under homotopy type theory can be carried directly into a formal, machine-checkable series of theorems and proofs, in the form of a Coq development.
To expect this material to be readable and useful to every average Joe right away is asking far too much of any new idea in mathematics. This is cutting edge research, and there is still too much even the people closest to this material don't understand yet. As another comment on yours alluded to, at one time your equivalent in the 1700s would have written off calculus as indecipherable and judged it not likely to succeed as a result.
Your comments in this thread have really piqued my interest enough to read some of this HoTT. I'd heard of this a couple of years back and didn't have the energy for it at the time.
Some years ago I spent a serious amount of time reading topos theory, particularly local set theory, as given by the Mitchell-Benabou internal language of any topos, looking for a better approach to description logics.
I do believe topos theory provides a better foundations than set theory because the logic is inherently intuitionistic. I found it also provided a simpler explanation of independence results. However one of the things I believe is true of the proof theory is that there is no cut-elimination theorem, which is important to establish a sub-formula property.
Sorry to ramble here, let me ask specifically, are there connections between HoTT and topos theory? Or geometric logic? Your earlier comment on the synthetic nature made me think there might be.
Thank you
Edit: I more or less answered my own question by reading the introduction, the section on open problems, the possible connections are between HoTT and the higher toposes. Judging from the intro, this seems very readable.
The original article is about a potential mathematical revolution, where computer verified proof has gone mainstream. The stuff about using weaker axiom systems, or getting theorems without needing AC is interesting, but I'd argue it is not so relevant. More important are things like this:
"The thing that’s so remarkable about this new foundation is that the fundamental concepts are much closer to where ordinary mathematicians do their work. In the usual foundation, Zermelo-Frankel set theory, it takes an enormous amount of work just to build up the basic concepts and theorems that mathematicians rely on every day. The result is that if you want a computer to check your proofs, you have to teach it all that theory first. Essentially, you have to give it the same education you got — except that you have to do it in a far more exacting way. As a result, the only people so far who have used computer proof systems are computer scientists who specialize in it, and it takes them many years of effort to check a single new theorem. Georges Gonthier, for example, spent a decade checking the four-color theorem.
But this approach circumvents all that labor. Not only that, but the language the computer understands is far closer to natural mathematical language."
I should point out that the Four-Colour Theorem was formalised in Coq, not a ZF-based proof assistant. But that aside, these are pretty big claims. I'd like to hear what sort of basic theory is being talked about, and how the proofs are closer to natural language. On the stackexchange thread, ek comments:
"Anyone who has used Coq will tell you that the proofs that you produce often don't end up looking much like equivalent plain-English proofs at all."
But this doesn't strike me as fair. I'm a HOL Light user, and the de facto proof style is procedural. In that style, which I understand is preferred also in Coq, the user tells the machine how to compose an assortment of automated tools to break down and solve the problem, often performing computations to massage the goal into a suitable form. The scripts are usually completely unreadable, but that's by design. Those who want a more readable style of formalised proof are encouraged to use "declarative styles".
How do the claims made about HoTT's readability factor in here?
>But this doesn't strike me as fair. I'm a HOL Light user, and the de facto proof style is procedural. In that style, which I understand is preferred also in Coq, the user tells the machine how to compose an assortment of automated tools to break down and solve the problem, often performing computations to massage the goal into a suitable form. The scripts are usually completely unreadable, but that's by design. Those who want a more readable style of formalised proof are encouraged to use "declarative styles".
It's possible to create readable coq scripts. However, like with any kind of programming it takes effort. If you take a look at the proof of four colors theorem of fiet thompson they are quite readable and don't look like complete mess. They, however, use modified coq instead which is called ssreflect.
To be clear, constructive mathematics is not new to me. I just don't see the point of it.
That mathematics can be done in a machine-checkable way was known long before HoTT. Nothing new there. For example, I've had no (particular) difficulty mechanising surreal numbers without using HoTT for this. Also real numbers can be done easily without HoTT. So again:
Why should I care about the univalence axiom?
If you cannot answer that, I am not sure you know what you are talking about. And also, maybe you are a little bit underestimating the links between HoTT and constructivism.
Since you are using the word "constructivism" so often, there is probably some sort of misunderstanding. Constructivism usually refers to the philosophical school of thought which rejects the axiom of excluded middle for fairly dogmatic reasons. Most people who learn about this are appalled, since excluded middle appears to be consistent and useful. In particular, intuitionistic set theory is weird and unintuitive - most people don't bother with it.
This has little to do with the reason for constructive logic in HoTT or any type theory. Models of type theory collapse if you add excluded middle and you cannot interpret the resulting structure in any particularly useful way. Without excluded middle you have more freedom in designing new axioms.
This is the reason why HoTT is constructive: You have a choice between classical logic and univalence. The latter turns out to be more useful.
You get a choice between univalence and excluded middle. The whole argument is that univalence is more useful in practice.
Briefly, in Martin-Löf type theory equalities are very strong, but you do not have many tools for proving new equalities. Univalence is one answer to this problem. So the choice is roughly between "having more equalities" (univalence) or "making everything decidable" (excluded middle).
Additionally, in HoTT you can embed classical set theory at "h-level 1". Basically, you get a slightly weaker form of excluded middle + choice, which is nevertheless sufficient for building a model of classical ZFC. The reverse is not possible, as far as I know.
In short: I don't get a choice between univalence and excluded middle, I HAVE to choose between univalence and excluded middle. Which is an easy choice for me: I choose excluded middle.
Sorry if I wasn't clear about this, but you can embed classical mathematics in a type theory with univalence. If you look into the HoTT book, there is a chapter on set theory in type theory. The general form of excluded middle is inconsistent, because it would collapse the structures on which univalence is built.
This means that classical mathematics still works as expected, so long as you have the assumption that you are working with things that are "set-like". Additionally you can make any type "set-like", since this amounts to manually collapsing its equality type.
However... the truth is that most of the time excluded middle is unnecessary (in a type theory). Having nice equality types is so much more useful that, honestly, you are not making an informed decision.
Answer to auggierose's comment above: Yes you can prove that sqrt(2) is irrational.
This is actually a great example, because it doesn't need excluded middle. Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work.
Edit: Ok, this was apparently confusing, so let me repeat it here. Yes, the same proof works. This form of excluded middle is entirely unproblematic.
There might be some confusion. The typical proof of the irrationality of root 2 is phrased as a proof-by-contradiction, and I've come across folk who mistakenly think that this technique is exclusive to classical mathematics.
In fact, the standard proof-by-contradiction that sqrt(2) is irrational is also intuitionistically valid. The important point for this case is that we're proving a negative property (irrationality), so this sort of proof by contradiction is fine.
The standard example of a classical proof I use is the one showing that there exist irrationals x and y such that x^y is rational. The dead easy proof asks whether x^y is rational for x=y=sqrt(2). If it is, we're done. Otherwise, we just take x=sqrt(2)^sqrt(2) and y=sqrt(2).
But note that we don't actually know for sure which x and y work, so this is definitely classical. An intuitionistic proof here would have to tell us directly what x and what y work.
Sigh. It is really hard to get straight answers out of constructivists / type theorists.
So let's say I am writing a theorem proving system based on HoTT (with univalence). Can I then do the classic proof of the irrationality of the square root 2 in that system? Then this would be classical mathematics as I expect it.
This is exactly the answer I expected. It was a little bit of a trap, I have to admit that.
I didn't ask for any proof of the irrationality of square root 2. I asked specifically for the classic proof. Which I cannot do. So it is not classic mathematics as usual.
An honest answer to this whole thread would have been: "No, you cannot do classical mathematics as you were used too. You have to give stuff up, but I think that you will gain other stuff in exchange, and in my opinion this other stuff is more valuable than the stuff you gave up."
Note that fmap writes: "Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work."
What is meant by "even if it wasn't, it would still work" goes back to something he said earlier: type theory embeds an infinite hierarchy of axioms of choice and laws of excluded middles. If you want to do propositional-like reasoning in homotopy type theory, you can assume AC or LEM for homotopy (-1)-types, corresponding to propositional logic.
In type theory you are encouraged to drop the law of the excluded middle and the axiom of choice, because of the fact that doing so gives you potentially more expressive ways of doing things as we have said, but you have gotten the impression that you have to, which you don't.
Also, the claim in this thread was that the results from classical mathematics are provable using homotopy type theory, not that they are provable in the same way (though that holds as well, as I've said above; it's just that the mathematics might not look as clean as if you did it in a more idiomatic way). This kind of a value proposition is not exactly new: category theory loses certain axioms over set theory and mathematicians adapted to the point that category theory is now the language of modern algebra.
I want to point out that I suggested that you read the introduction to the book because it provides these same answers to the questions you are wondering about. I still suggest you do so, as it goes into more detail on what we have said here in a way that I am not able to quite as well.
I already read the introduction a couple of months ago, pretty much on the day when they officially announced that the book is available.
From what I understand: If you are a type theorist / constructivist, then certain constructions will not be provably equivalent, although their classical counterparts are. Some of those classically trivial equivalences might be recovered though via the univalence axiom. Is that correct or totally wrong? Furthermore it seems to me from the discussions with fmap, that if I am a classical mathematician, I cannot use HoTT (unless I am willing to compromise and give up some of my power).
Your understanding of univalence seems essentially correct to me.
At this point we are mostly debating what "can use" means -- it's probably enough to say that unless you reframe your thinking, perhaps radically, probably it will be hard for you to be able to use HoTT to get work done. It is possible to do classical mathematics within HoTT, in the normal way, but it would not be very fun.
Yes :) My interest in homotopy type theory is only auxiliary to my research. Designing dependent type systems in a way that balances tractability with expressiveness is a pretty hard thing to do. SMT solvers are nice because you can treat them as oracles and "see what happens". I'm not an expert on decision procedures, and I'd characterize myself more as a user of solvers than a developer of them, though of course once you get deep enough in, that line blurs.
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.
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 .
> 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.
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?
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.
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.
> 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.
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.
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.
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.
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.
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:
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.
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...
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.
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.
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.
> 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.
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.
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.
It's the difference between showing that a candidate proof is correct, and coming up with a correct proof in the first place. Once you have a proof, showing it is correct is (easily) computable. But coming up with a correct proof in the first place is not computable in general. (More generally, deciding whether a given proposition is true -- i.e. whether a proof exists or not -- is not computable. That is the "entsheidungsproblem".)
thanks. after reading your explanation it's clear that the verification is verification of the proof, whereas i was interpreting it as verification of the statement to be proved, hence my confusion.
Until I read your post, it never occurred to me you were confused by the ambiguous implications of "verification".
You remind me how easy it is, once you get the jargon and the concepts, to not actually write out everything into a form someone from the outside can understand.
Verification is saying that a given proof does substantiate a theorem—it's easy as it's "just" a special kind of type-checking algorithm. Provability is saying that given some theorem it's possible to find a proof in a particular axiomatic system.
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.
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.
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?
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
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.
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...
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?
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.
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.