Interestingly, HOL Light is used to prove that the density of a packing of congruent spheres in three dimensions is never greater than pi/sqrt(18), a 400 year old problem:

https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet

300,000 lines of code, still unfinished.