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.

Just this Sunday, Hales and his team announced that the 300 pages of proof had been scrutinized by the pair of programs and, to his relief, it's all correct. In other words, the computer successfully verified that the idea put forward by Kepler over 400 years ago is right. "I suddenly feel ten years younger," Hales told New Scientist.

But it's not just good news for Hales. There are hundreds of ridiculously dense mathematical proofs created every year, and this demonstrates that they can checked by computers rather than humans. That means that mathematicians can now concentrate on thinking creatively about their problemsâ€”and let computers do the grunt work of checking to make sure they're correct. [New Scientist]

Advertisement

*Image by dexter_mixwith under Creative Commons license.*