[math-ias] REMINDER: Members Seminar -- TODAY (Monday, November 26, 2012)

[Dottie Phares]

REMINDER:


Members Seminar


 


Topic:

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


Speaker:

Daniel Licata


Affiliation:

Carnegie Mellon University; Member, School of Mathematics


Date:

Monday, November 26


Time/Room:

2:00pm - 3:00pm/S-101

  _____  

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.

 

 

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://imap.math.ias.edu/mailman/private/all/attachments/20121126/439a4d0a/attachment-0002.html>