| 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
|
