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 per cent 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 be 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]
Picture: dexter_mixwith