DanColloquium - Macaulay2/Workshop-2015-Boise GitHub Wiki

Thursday, May 28, 2:00-2:50pm, room MB 139

Title: Homotopy Type Theory and Univalent Foundations

Speaker: Daniel R. Grayson (UIUC)

Abstract:

Homotopy type theory with the univalence axiom of 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 sets are defined in terms of a more primitive notion called "type". 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. With a semantic interpretation in homotopy theory, it offers an alternative world where the proofs of basic theorems of mathematics can be formalized with minimal verbosity and verified by computer.

As a relative newcomer to the field, I will survey these recent developments and sketch the basic concepts for a general mathematical audience.

About the speaker: In addition to being one of the authors of Macaulay2, Professor Grayson also helped write Mathematica.