School of Mathematics

Introduction to the Coq Proof Assistant

Andrew Appel
Princeton University
December 7, 2010

A "proof assistant" is a software package comprising a validity checker for proofs in a particular logic, accompanied by semi-decision procedures called "tactics" that assist the mathematician in filling in the easy parts of the proofs. I will demonstrate the use of the Coq proof assistant in doing simple proofs about inductive structures such as natural numbers, sequences, and trees.

A Reidemeister-Singer Conjecture for Surface Diagrams

Jonathan Williams
University of California, Berkeley
December 3, 2010

There is a way to specify any smooth, closed oriented four-manifold using a surface decorated with simple closed curves, something I call a surface diagram. In this talk I will describe three moves on these objects, two of which are reminiscent of Heegaard diagrams for three-manifolds. These may form part of a uniqueness theorem for such diagrams that is likely to be useful for understanding Floer theories for non-symplectic four-manifolds.