Via Neighborhood of Infinity, I came across the Flyspeck Project, a project to provide a computer-checked proof of the Kepler conjecture.

The project who proposed by Thomas Hales, who has the only published proof of the theorem. His proof already includes some computer calculations, and turned out to be too complicated to be fully checked by peer review. A complete computer-checked proof would remove any doubts.

The Wikipedia entry links to this elementary introduction by Hales to the proof, Cannonballs and Honeycomb.

Pingback: Ars Mathematica » Blog Archive » Machine-Checkable Proofs