Voevodsky's Univalent Foundations for mathematics

Mathematical Conversations
Topic:Voevodsky's Univalent Foundations for mathematics
Speaker:Daniel Grayson
Affiliation:University of Illinois at Urbana-Champaign; Visitor, School of Mathematics
Date:Wednesday, January 25
Time/Room:6:00pm - 7:00pm/Dilworth Room

We'll take a glance at the world of mathematics as viewed through the Univalent Foundations of Voevodsky. In it, "set" and "proposition" are defined in terms of something more fundamental: "type". The formal language fulfills the mathematicians' dream: one cannot even express a property that fails to be invariant under isomorphism. Moreover, it offers the hope that formalization (and thus verification) of today's mathematical knowledge may be accessible.