Univalent Foundations: New Foundations of Mathematics - Vladimir Voevodsky

Vladimir Voevodsky explains how univalent foundations bridge constructive mathematics, type theory, and computer-assisted proof verification.

Vladimir Voevodsky Institute for Advanced Study; Faculty, School of Mathematics March 26, 2014 In Voevodsky’s experience, the work of a mathematician is 5% creative insight and 95% self-verification. Moreover, the more original the insight, the more one has to pay for it later in self-verification work. The Univalent Foundations project, started at the Institute a few years ago, aims to lower the price by giving mathematicians the ability to verify their constructions with the help of computers. Voevodsky will explain how new ideas that make this goal attainable arise from the meeting of two streams of development—one in constructive mathematics and the theory and practice of programming languages, and the other in pure mathematics. The Institute for Advanced Study is pleased to designate this lecture in honor of the Princeton Adult School’s 75th Anniversary. The Institute supports and shares the Adult School’s mission to promote and foster lifelong learning and exploration in the Princeton community and beyond. The lecture is free and open to the public, and seating is on a first-come, first-served basis. For more videos, visit video.ias.edu