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 o

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 https://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet 300,000 lines of code, still unfinished.