Univalent Foundations: New Foundations of Mathematics [video](video.ias.edu)
video.ias.edu
Univalent Foundations: New Foundations of Mathematics [video]
https://video.ias.edu/node/6365
6 comments
This is a great and insightful comment. May I just clarify, you say you are a "PL theorist"—is that programming language theorist? What kind of work does that entail?
You said it much better than I could. I also think their intimations that mathematicians will use computers to ensure their theorems are correct will not come to fruition, though they are selling it as a huge advantage.
This is a very interesting project and it has actually set me on an interesting path.
In scientific computation one blends mathematics and computation. The math is highly advanced, and it will tell you important things about your resulting code such as what kind of stability properties you should expect, and how "robust" the code is (deliberately ambiguous term, but in most cases it means: does your code work equally well no matter what parameters you throw at it?).
In the realm of physics simulations, these math questions turn out to be amazingly delicate and failing to answer them before running your code on a very large problem very often leads to unexpected (and wrong) results, if the code actually ever successfully finishes executing.
There is therefore a tremendous amount of literature where these questions are answered, all containing a meticulous amount of careful detail as well as deep insights coming from all the relevant branches: linear algebra, physics, functional analysis.
The problem however is that as we gain more understanding and knowledge the math hasn't gotten any easier. Sometimes the arguments are so sophisticated that it really leads me to doubt whether the result can be trusted at all.
This leads into something which I know very little:
A better understanding of foundations really is called for here, and a foundation which lends itself better to computation than what is currently available. Computers need to start being able to verify proofs better. Proof assistants exist today, but their use is currently limited to computer scientists because they rely on deep results in that field relating type theory to mathematics - it represents a tremendous barrier to practicing mathematicians.
I hope in the future that "reproducibility" in my field means not only submitting your code so that other people can reproduce your performance claims, but submitting proof documents to be independently verified on someone else's computer. Whenever I read the small bits about univalent foundations it sounds like they are adding magic sauce to make this possible, and so I follow it closely (but don't understand it all yet).
The interesting path I spoke of earlier: I'm now learning type theory and functional programming just so that I can make sense of this branch of computer science that I originally didn't know existed.
In scientific computation one blends mathematics and computation. The math is highly advanced, and it will tell you important things about your resulting code such as what kind of stability properties you should expect, and how "robust" the code is (deliberately ambiguous term, but in most cases it means: does your code work equally well no matter what parameters you throw at it?).
In the realm of physics simulations, these math questions turn out to be amazingly delicate and failing to answer them before running your code on a very large problem very often leads to unexpected (and wrong) results, if the code actually ever successfully finishes executing.
There is therefore a tremendous amount of literature where these questions are answered, all containing a meticulous amount of careful detail as well as deep insights coming from all the relevant branches: linear algebra, physics, functional analysis.
The problem however is that as we gain more understanding and knowledge the math hasn't gotten any easier. Sometimes the arguments are so sophisticated that it really leads me to doubt whether the result can be trusted at all.
This leads into something which I know very little:
A better understanding of foundations really is called for here, and a foundation which lends itself better to computation than what is currently available. Computers need to start being able to verify proofs better. Proof assistants exist today, but their use is currently limited to computer scientists because they rely on deep results in that field relating type theory to mathematics - it represents a tremendous barrier to practicing mathematicians.
I hope in the future that "reproducibility" in my field means not only submitting your code so that other people can reproduce your performance claims, but submitting proof documents to be independently verified on someone else's computer. Whenever I read the small bits about univalent foundations it sounds like they are adding magic sauce to make this possible, and so I follow it closely (but don't understand it all yet).
The interesting path I spoke of earlier: I'm now learning type theory and functional programming just so that I can make sense of this branch of computer science that I originally didn't know existed.
You might be interested in Edward Kmett's automatic differentiation[0] package, ad[1]. It is one of my favorite non-trivial blendings of computer science techniques and more traditional mathematics. In specific, it uses Haskell's type system to prevent subtle numerical errors which other automatic differentiation libraries require the user to prevent by being very careful. The resulting code is much more trustworthy.
[0] http://en.wikipedia.org/wiki/Automatic_differentiation [1] https://github.com/ekmett/ad/
[0] http://en.wikipedia.org/wiki/Automatic_differentiation [1] https://github.com/ekmett/ad/
I'm not sure if it's really the foundations that are the biggest barrier to entry for mathematicians (at least for most fields of math). Admittedly, I don't have experience with dependent-type based systems such as Coq/Agda, which, incidentally, are what the authors use to formalize their Univalent Foundations. But at least for HOL-based systems (e.g. Isabelle/HOL or HOL4), you don't really need to understand their foundations in order to work with them. Oddly enough, they're neither the standard (first-order, that is, predicate logic based) ZFC theory, nor the Univalent foundations.
Isabelle in particular already has reasonably large formalizations of classic results in analysis and linear algebra. It also has a nice structured input language which makes the proofs relatively similar to the standard mathematical language. Here's a formalization of the Hahn-Banach theorem (a central result of functional analysis):
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/H...
(the rendering is not complete, as many special symbols aren't replaced in the HTML version - it looks nicer when opened in Isabelle itself). If you're interested in learning more, you can start with the "new" tutorial:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2...
Anyway, I think that computer proofs are going to remain harder for the foreseeable future, no matter what the foundations. Human written proofs tend to skip and conflate many small steps, and this is exactly what makes them easier and faster to write. Ideally, the verification system would perform this small steps automatically on your behalf. They're getting better at that (the sledgehammer tool in Isabelle is great), but still very far away from what you'd need.
Until that happens I don't expect to see pervasive machine-assisted proofs anywhere. Not least because of the dynamics of modern academia. It's publish or perish, and if doing computer proofs slows you down, a lot of people are going to chose not to do them, and this sets a standard in the field (where such proofs are not particularly valued).
The whole post of course comes with a big caveat: I'm not familiar with Univalent Foundations (I watched the video but that doesn't really discuss them). If I'm wrong in my views I would love some UF experts to chime in.
Isabelle in particular already has reasonably large formalizations of classic results in analysis and linear algebra. It also has a nice structured input language which makes the proofs relatively similar to the standard mathematical language. Here's a formalization of the Hahn-Banach theorem (a central result of functional analysis):
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/H...
(the rendering is not complete, as many special symbols aren't replaced in the HTML version - it looks nicer when opened in Isabelle itself). If you're interested in learning more, you can start with the "new" tutorial:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2...
Anyway, I think that computer proofs are going to remain harder for the foreseeable future, no matter what the foundations. Human written proofs tend to skip and conflate many small steps, and this is exactly what makes them easier and faster to write. Ideally, the verification system would perform this small steps automatically on your behalf. They're getting better at that (the sledgehammer tool in Isabelle is great), but still very far away from what you'd need.
Until that happens I don't expect to see pervasive machine-assisted proofs anywhere. Not least because of the dynamics of modern academia. It's publish or perish, and if doing computer proofs slows you down, a lot of people are going to chose not to do them, and this sets a standard in the field (where such proofs are not particularly valued).
The whole post of course comes with a big caveat: I'm not familiar with Univalent Foundations (I watched the video but that doesn't really discuss them). If I'm wrong in my views I would love some UF experts to chime in.
Vladimir Voevodsky received Fields medal in 2002, so please note that it's not usual amateurish try to create new mathematics while knowing nothing about the old one.
Please remember to append "[video]" to the title when it's a video.
Just when I found myself starting to lean in he started skipping slides. Most frustrating.
Does anyone have another link? For some reason its dead.
Now, at this point a lot of programming-oriented people get confused, because they think, "how can you ever change the foundations? How can you do any math at all until you've completely formally defined the foundations of the subject?" This is a philosophical question, but in truth foundations of math aren't as hugely important as you might think. Here's an analogy: on both Windows and Linux you can write an email client. Now, the process will not be identical: some things that are easy on Windows are harder on Linux, and vice versa. But at the end of the day, the result on either platform will recognizable be an email client, and your major challenges will probably be email challenges, not platform challenges. Most mathematicians do not work at the foundations—they work at foundations for their specific field (a ring theorist cares about the properties of rings, not often the properties of sets, for example). You can analogize this to using a framework, like GTK for example.
On the other hand, some subjects are poorly served by certain foundations, and some of the newer subjects in mathematics are running into that problem. The most pressing examples are category theory and homotopy theory, both of which are based on a study of operations, not objects, in a technical way that is poorly served by the current consensus foundation for mathematics. This would be like really wanting to write mobile apps—Windows would not be a good platform for it, and Android would be. As a PL theorist and kind-of-mathematician, I think the work going on in the Univalent Foundations project to be really interesting and extremely beautiful. I think it will have a profound impact on our understanding of mathematical foundations and higher-order logic, and I'm excited to see what comes of this effort. But I don't think it will really impact mathematics all that much—the impact of categorical thinking is the really important change, and that is helped, but not much, by new foundations.