DIMACS - RUTGERS EXPERIMENTAL MATHEMATICS SEMINAR

Sponsored by the Rutgers University Department of Mathematics and the
Center for Discrete Mathematics and Theoretical Computer Science (DIMACS)

Co-organizers:

Drew Sills, Rutgers University, asills {at} math [dot] rutgers [dot] edu

Doron Zeilberger, Rutgers University, zeilberg {at} math [dot] rutgers [dot] edu

Title: Formal proofs, the four-color theorem, and the Kepler conjecture for sphere packings

Speaker: Tom Hales, University of Pittsburgh

Date: October 6, 2005 5:00pm

Location: Hill Center, Room 705, Rutgers University, Busch Campus, Piscataway, NJ

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. Last year, 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 a number of interesting connections with my current work on packing spheres.