Way back in 1611, Johannes Kepler suggested that the most efficient way to stack spheres—like arranging oranges for sale—was in a pyramid formation. Sadly, he couldn't prove it, but now a computer has finally verified it to be true, settling centuries of debate.
In fact, Thomas Hales of the University of Pittsburgh, Pennsylvania, developed a proof for the problem back in 1998. But at 300 pages, it took 12 reviewers four years to check for errors—and even then, they were only 99 percent certain it was correct. So, in 2003, Hales began to create the Flyspeck project: a computational tool that would check his proof.
It uses two pieces of formal verification software—delightfully called Isabelle and HOL Light—both of which rely on just a small, easily validated series of logical statements. With those, they can check any series of other logical statements, like a mathematical proof, if they have enough time.
To read the rest of the story, please go to: Gizmodo
