The solution of the Kepler's conjecture by Hales deserves a special answer since it gives an important example both for a proof to a mathematical theorem massively using computers, and 15 years later by an impressive project for demonstrating a formal proof for the conjecture that could be automatically verified.

The problem and the first project which in part was carried out by Hales with Ferguson is described in the Notices AMS paper "Cannonballs and Honeycombs" Another reference is a 2002 ICM survey A Computer Verification of the Kepler Conjecture.

The published account of the second project - The Flyspeck project can be found in the paper A formal proof of the Kepler conjecture.

For more information and links, see Hales homepage.

The solution of the Kepler's conjecture by Hales deserves a special answer since it gives an important example both for a proof to a mathematical theorem massively using computers, and 15 years later by an impressive project for demonstrating a formal proof for the conjecture that could be automatically verified.

The problem and the first project which in part was carried out by Hales with Ferguson is described in the Notices AMS paper "Cannonballs and Honeycombs" Another reference is a 2002 ICM survey A Computer Verification of the Kepler Conjecture.

The published account of the second project - The Flyspeck project can be found in the paper A formal proof of the Kepler conjecture.

For more information and links, see Hales homepage.