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.