Dan Grayson (University of Illinois at Urbana-Champaign) will give an intuitive introduction to the recent developments within the field at the University of Oslo.

Homotopy type theory, with the partition of types into levels and the univalence axiom developed by Voevodsky, provides both a new logical foundation for mathematics (Univalent Foundations) and a formal language usable with computers for checking the proofs mathematicians make daily.  As a foundation, it replaces set theory with a framework where propositions and sets are defined in terms of a more primitive notion called "type" -- in this framework the notion of symmetry arises at the most basic level: from the logic. As a formal language, it encodes the axioms of mathematics and the rules of logic simultaneously, and promises to make the extraction of algorithms and values from constructive proofs easy. As a mathematical topic, it offers an intriguing range of open problems at all levels of accessibility.

Coffee, tea, and biscuits will be served from 2 pm.