School of Mathematics

Mechanizing the Odd Order Theorem: Local Analysis

Georges Gonthier
INRIA, France
January 20, 2011

Abstract: In addition to formal definitions and theorems, mathematical theories also contain clever, context-sensitive notations, usage conventions, and proof methods. To mechanize advanced mathematical results it is essential to capture these more informal elements. This can be difficult, requiring an array of techniques closer to software engineering than formal logic, but it is essential to obtaining formal proofs of graduate-level mathematics, and can give new insight as well.

Contacting the Moon

Urs Frauenfelder
Seoul National University
January 19, 2011


The restricted 3-body problem has an intriguing dynamics. A deep observation of Jacobi is that in rotating coordinates the problem admits an integral. In joint work with P. Albers, G. Paternain and O. van Koert, we proved that the corresponding energy hypersurfaces are contact for energies below and slightly above the first critical value.

Moment-Angle Complexes, Spaces of Hard-Disks and Their Associated Stable Decompositions

Fred Cohen
University of Rochester; Member, School of Mathematics
January 10, 2011

Topological spaces given by either (1) complements of coordinate planes in Euclidean space or (2) spaces of non-overlapping hard-disks in a fixed disk have several features in common. The main results, in joint work with many people, give decompositions for the so-called "stable structure" of these spaces as well as consequences of these decompositions.

This talk will present definitions as well as basic properties.

Two Dimensional Galois Representations Over Imaginary Quadratic Fields

Andrei Jorza
Institute for Advanced Study
December 16, 2010

To a regular algebraic cuspidal representation of GL(2) over a quadratic imaginary field, whose central character is conjugation invariant, Taylor et al. associated a two dimensional Galois representation which is unramified at l different from p outside a finite set of places. The first half of this talk concerns the crystallinity of the Galois representation at p , under a technical assumption. The second half of the talk is on recent work towards local-global compatibility (on GSp(4) and its implication for GL(2)).

Colouring Tournaments

Paul Seymour
Princeton University
December 13, 2010

A ``tournament'' is a digraph obtained from a complete graph by directing its edges, and ``colouring'' a tournament means partitioning its vertex set into acyclic subsets (``acyclic'' means the subdigraph induced on the subset has no directed cycles). This concept is quite like that for graph-colouring, but different. For instance, there are some tournaments H such that every tournament not containing H as a subdigraph has bounded chromatic number. We call them ``heroes''; for example, all tournaments with at most four vertices are heroes.