Dan Grayson (Illinois): An introduction to formalization of proofs in UniMath

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.