What if Current Foundations of Mathematics are Inconsistent? | Vladimir Voevodsky
Why Hacker News recommends it
Recommended as a thought-provoking lecture from a Fields medalist on the foundations of mathematics and formal proof verification.
What it is
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 by 3 HN commenters across 3 different months, 2017 to 2019.
What Hacker News said
Recommends Ericson2314 · 2017-11 · on “How a destructive idea paved the way for modern math”
Yes we must take saxioms on faith alone. Embrace pluralism and move on. [this video] by the late great Voedvodvosky is more interesting.
Recommends IngoBlechschmid · 2018-11 · on “Mystery Math Whiz and Novelist Advance Permutation Problem”
> 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 pr
Recommends ukj · 2019-07 · on “A Programmer’s Regret: Neglecting Math at University”
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.