A Famous Mathematician

                          Sventeenth century Mathematician Johannes keplar defined some basic

rules for the how the planets move, and g iven his predilections for contemplating spheres,

he suggested in 1611 that the most efficient way to stack spheres was in a pyramid

formation.But he was unable to prove it in a mathematically satisfactory way, and the idea

remained unproven for 400 years.

                         New Scientist reports that a scientist named Thomas Hales successfully

confirmed Kepler's hypothesis to be true this past Sunday with help from a computer.Hales

first proved it himself by hand in a 300-page paper in 1998, but his solution was only

deemed 99% certain to be correct.

                   He enlisted help from computers under Isabelle and HOL Light, went to work

formally validating each of the steps in logic required to arrive at the conclusion that

spheres are most efficiently arranged in a pyramid shape.

                   Hales is glad at having his hard work confirmed to be totally correct, but the real

significance of the Flyspeck Project is that computers can do the tedious work of double-

checking logical proofs while mathematicians are left to ponder their next great problems.

                   This technology cuts the mathematical referees out of the verification process,

Hales told New Scientist. "Their opinion about the correctness of the proof no longer

matters."Grocers around the world rejoice as they continue stacking oranges the way they

always have.   more information >>