Event Title: OR
Speaker Last Name:    OR
Year: (yyyy)

Mathematics Colloquium


Date:  Tuesday, February 21, 2006

Title:  Formal Proofs, the Four Color Theorem, and the Kepler Conjecture for Sphere Packings

Abstract:  The four color theorem states that any map can be colored with four colors in such a way that adjacent countries do not receive the same color. This theorem is one of the most famous math problems ever to be solved by computer. Recently, Georges Gonthier gave a completely formal proof of the four color theorem. This means the proof has now been carefully checked at the level of fundamental axioms and rules of inference of mathematics. I will describe Gonthier's project and explain connections with my current work on packing spheres.

Speaker:  Tom Hales
Institution:  University of Pittsburgh


Back to current Colloquium List
Back to UM Math seminars page


Department of Mathematics   |   2074 East Hall   |  530 Church Street  
Ann Arbor, MI 48109-1043
Phone: 734.764-0335   |   Fax: 734.763-0937

The page last modified
Site errors should be directed to