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.
The classical Dvoretzky theorem asserts that for every integer k>1 and every target distortion D>1 there exists an integer n=n(k,D) such that any
In recent research it has become clear that there are fascinating connections between constructive mathematics, especially as formulated in the type theory of Martin-Löf, and homotopy theory, especially in the modern treatment in terms of Quillen model categories and higher-dimensional categories. This talk will survey some of these developments.
ANALYSIS/MATHEMATICAL PHYSICS SEMINAR
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.