Institute for Advanced Study
3 HN recommenders · recommended in 3 months, 2017–2019
58:30 · 57K views · Apr 26, 2012
Vladimir Voevodsky's IAS lecture starts from Godel's second incompleteness theorem to explore whether first-order arithmetic could be inconsistent. It motivates his vision of univalent foundations and computer-checked proofs.
Recommended as a thought-provoking lecture from a Fields medalist on the foundations of mathematics and formal proof verification.
3 comments from Hacker News
> And indeed, this will likely always be the case, as the true purpose of proving a mathematical result is almost never to actually get the boolean true/false output, but to illustrate how to solve the problem in the first place and what methods were helpful for that. As a working mathematician, I wholeheartedly agree with the second part of the quoted sentence! But I think that the first part isn't quite right: The function of proofs to determine truth is extremely important, especially considering that, especially in pure mathematics, we often can't check our results in any other manner (like conducting physical experiments or checking many cases with the computer). Bad experiences with proofs which later turned out to be faulty led Voevodsky to initiate his univalent foundations program (also called homotopy type theory ), where all results should be checked by the computer. (For the particular area he was working on, no existing theorem prover turned out to be sufficient. He made a breakthrough in finding a new foundation to base theorem provers on, which made it possible to formalize results in his area of mathematics not only in principle, but also in practice.) The hope is also that with computer-checked proofs, we can advance to new areas of mathematics which are currently inprenetable to our puny human minds. I'm very much looking forward to this future! You can learn more about Voevodsky's vision in slides of him and in a recorded lecture: [LINK] this video
Where Hilbert erred was looking for foundations in first-order logic. Univalent foundations are laid on high-order logic. It's the distinction between top-down and bottom-up thinking. If you are into philosophy/epistemology - it's somewhat of an attempt to shift Mathematics from foundationalism towards structuralism. I recommend this video: this video Hilbert's dream of Metamathematics has sort of come true in the form of homoiconicity in programming languages.
Yes we must take saxioms on faith alone. Embrace pluralism and move on. this video by the late great Voedvodvosky is more interesting.