The Flyspeck Project

I just came across the Flyspeck Project. The problem they are dealing with is the verification of the Kepler conjecture. Although there is a potential proof nobody is 100% sure of its validity and it seems that the group asigned to verify it have run out of steam. So the Flyspeck Project seeks to build a complete formal proof using HOL Light, a computational framework for proving things. Unfortunately the guys behind the project expect it might take as long as twenty years to verify the potential proof. Let's hope that not too many interesting conjectures require this treatment.

Note that this is different from the four colour problem. For that problem, the proof required an enumeration that was too long and complicated to carry out by hand, so a machine carried it out. For this problem we have a slightly different situation: we already have a potential proof, but we need to reduce it to a completely formal form so that the entire thing can be verified to follow from axioms.