# HoTT Coq

June 9, 2015 10:40 PM Subscribe

Univalent Foundations Redefines Mathematics - "When a legendary mathematician found a mistake in his own work, he embarked on a computer-aided quest to eliminate human error. To succeed, he has to rewrite the century-old rules underlying all of mathematics." (previously)

Voevodsky's Univalence Axiom in Homotopy Type Theory

-Homotopy Type Theory and Higher Inductive Types

-Univalent Foundations of Mathematics

also btw...

-James Simons interview

-Univalent Foundations: "No Comment." (via)

-There's more to mathematics than rigour and proofs

Voevodsky's Univalence Axiom in Homotopy Type Theory

One of Voevodsky's goals (as we understand it) is that, in a not too distant future, mathematicians will be able to verify the correctness of their own papers by working within the system of univalent foundations formalized in a proof assistant and that doing so will become natural even for pure mathematicians (the same way that most mathematicians now typeset their own papers in TeX). We believe that this aspect of the univalent foundations program distinguishes it from other approaches to foundations by providing a practical utility for the working mathematician.-Type Theory: A Modern Computable Paradigm for Math

-Homotopy Type Theory and Higher Inductive Types

-Univalent Foundations of Mathematics

also btw...

-James Simons interview

-Univalent Foundations: "No Comment." (via)

-There's more to mathematics than rigour and proofs

*And this reminds me of a quite different concern I have — this is MH speaking now, not the panelists — about computer-verifiable proofs: the prospect of technological lock-in.*

If there is an isomorphism that translates an existing human-written proof to a computer-written proof, isn't the same possible in the other direction, which eliminates "lock-in"?

posted by a lungful of dragon at 11:46 PM on June 9, 2015

Look at the proof of the four-color theorem for an example of the kind of thing they're concerned about, I think.

posted by NMcCoy at 12:10 AM on June 10, 2015

posted by NMcCoy at 12:10 AM on June 10, 2015

As I understand it, these proofs aren't exactly computer written, they are written in cooperation with a proof assistant. Coq is probably the one most associated with HoTT, but Nuprl is quite interesting as well. You provide input and then the proof assistant uses various "tactics" to try to prove what you've written based on existing proofs. When it gets stuck it asks for help by printing the statement it is stuck on, you give a hint and it tries again.

So they really are human readable, just requires a different set of skills. With a bit of UX work it may even end up being more human friendly than the classical approach.

Bonus: Four-Color Theorem via Coq

posted by ethansr at 12:16 AM on June 10, 2015 [1 favorite]

So they really are human readable, just requires a different set of skills. With a bit of UX work it may even end up being more human friendly than the classical approach.

Bonus: Four-Color Theorem via Coq

posted by ethansr at 12:16 AM on June 10, 2015 [1 favorite]

I hate this FPP's title, but also I love this FPP's title

posted by DoctorFedora at 1:12 AM on June 10, 2015 [2 favorites]

posted by DoctorFedora at 1:12 AM on June 10, 2015 [2 favorites]

I'm sorry, Doctor Fedora, Coq won't allow that statement as it stands. Univalence permits only love and the successor to love!

posted by No-sword at 1:42 AM on June 10, 2015 [5 favorites]

posted by No-sword at 1:42 AM on June 10, 2015 [5 favorites]

Math Nerd!

posted by Nanukthedog at 5:28 AM on June 10, 2015

posted by Nanukthedog at 5:28 AM on June 10, 2015

*Set theory begins with the set containing nothing — the null set — which is used to define the number zero.*

Wait, are we talking about set theory, ZFC, or talking so far down to the reader as to imply they're the same thing? Sloppy article, f----- would not read again.

posted by 7segment at 6:45 AM on June 10, 2015

Can someone explain this for idiots like me? What is this, why is it important, and is it as big of a deal as the articles seem to make it?

posted by Sangermaine at 6:51 AM on June 10, 2015

posted by Sangermaine at 6:51 AM on June 10, 2015

It's a bit like trying to find the Theory of Everything for mathematics, a foundation upon which everything else is built. Bertrand Russell tried to do it using set theory but failed. Type theory might be the answer.

An interesting way my lecturer put it, during his class on type theory, is that it turns out that mathematics (which can be said to be mostly founded upon set theory) is actually a sub-discipline of computer science (which via programming language theory is founded upon type theory / category theory).

[disclaimer: IANA mathematician, but I'm somewhat familiar with type theory in relation to programming language theory and logic]

posted by destrius at 6:58 AM on June 10, 2015

An interesting way my lecturer put it, during his class on type theory, is that it turns out that mathematics (which can be said to be mostly founded upon set theory) is actually a sub-discipline of computer science (which via programming language theory is founded upon type theory / category theory).

[disclaimer: IANA mathematician, but I'm somewhat familiar with type theory in relation to programming language theory and logic]

posted by destrius at 6:58 AM on June 10, 2015

The argument above is the Curry-Howard isomorphism, which draws a parallel between writing a program that produces a value with a specific type and creating a proof of a mathematical theorem represented by that type.

posted by perihare at 7:48 AM on June 10, 2015

posted by perihare at 7:48 AM on June 10, 2015

I haven't read the article yet, but I've heard of Computer Aided Proofs and Coq in particular. At my new job, one of the interns is going to school for math and I asked him if he'd heard of Coq, which he hadn't yet, so I got to turn him on to the idea. Now, ask me what any of it means or how to use it and I'm lost, but hey - it made me feel a little smart for a few seconds at least ;)

Speaking of Type theory and Set theory... What's the difference between them? I thought that in many ways they were the same thing? I suppose I'll look into the Curry-Howard isomorphism. I'm sure I've seen it before in my meanderings, but didn't grok the details enough.

posted by symbioid at 9:53 AM on June 10, 2015

Speaking of Type theory and Set theory... What's the difference between them? I thought that in many ways they were the same thing? I suppose I'll look into the Curry-Howard isomorphism. I'm sure I've seen it before in my meanderings, but didn't grok the details enough.

posted by symbioid at 9:53 AM on June 10, 2015

Hey, this is what I'm working on right now! Sorry to self-link, but if you're interested in learning about this stuff we have a Primer on Homotopy Type Theory available as a free download at the webpage for our research project at the University of Bristol. Whereas the book linked in the post (produced by the group at IAS Princeton mentioned in the Quanta article) is very technically advanced, our Primer is intended to be a very slow and gentle introduction to the elementary ideas of the subject and doesn't assume any prior knowledge. We spell out the core of the language of HoTT and explain how to think about it, and show how to use it to do some basic logic.

posted by logopetria at 2:11 PM on June 10, 2015 [10 favorites]

posted by logopetria at 2:11 PM on June 10, 2015 [10 favorites]

« Older Hobbes was a manifestation of pure, unadulterated... | The most important new trade agreement is also the... Newer »

This thread has been archived and is closed to new comments

posted by brambleboy at 11:43 PM on June 9, 2015