Dan Grayson (University of Illinoise at Urbana-Champaign) has been invited to speak at the univerity of Oslo once more.

Grayson is a fellow on Homotopy Type Theory and Univalent Foundations.

Abstract: Voevodsky's Univalent Foundations, which I spoke about in the colloquium in November, has been implemented on the computer in a project called UniMath, whose goal is to formalize a substantial body of modern mathematics.  One of my chief goals is to formalize the result in a preprint of mine on a certain construction of long exact sequences of higher algebraic K-groups by purely algebraic means, with no homotopy theory.  In this talk, I intend to give a gentle introduction to Univalent Foundations and UniMath, the category theory underlying Quillen's K-theory, the statement I hope to verify (thereby relieving the referee of the job), and what some formalized proofs look like on the computer.