A Computer-Checked Proof that the Fundamental Group of the Circle is the Integers

This talk is designed for a general mathematical audience; no prior knowledge of type theory is presumed.
One of the main goals for the special year on univalent foundations is the development of a logical formalism, called homotopy type theory, which supports computer-checked mathematical proofs. The most basic advantage of this approach is that, when proofs are expressed in type theory, a computer program called a proof checker can automatically determine whether or not a proof is correct. To verify a theorem, a reader (or journal article reviewer!) need only understand the theorem statement and the definitions it depends on, and can delegate the task of checking the proof to the computer. Proof checkers are also useful aids for developing proofs: typically, one writes a proof interactively, allowing the computer to do some of the work of proving.
However, to make this approach useful in practice, the language for expressing proofs must be high-level enough that the time spent representing a proof in type theory is not prohibitive. The univalent foundations program adds several new ideas to type theory, which raise the level of abstraction at which mathematicians can work. In this talk, I will show how these ideas play out on a simple example, a proof that the fundamental group of the circle is the integers. Mike Shulman developed the first proof of this result in homotopy type theory; my proof is an adaptation of his, which uses the type theoretic concept of "path induction" to simplify the proof. Though this example proves a very basic result, it illustrates many of the key ideas of our approach: First, spaces-up-to-homotopy can be described in a direct, logical way, which captures their inductive nature. Second, Voevodsky's univalence axiom plays an essential role in the definition of the universal cover of the circle. Third, the proof has computational content: it can also be seen as a program that converts a path on the circle to its winding number, and vice versa. Fourth, the proof illustrates the interplay between homotopy theory and type theory, mixing ideas from traditional homotopy-theoretic proofs of the result with techniques that are common in type theory.