Proof confirmed of 400-year-old fruit-stacking problem
- 11:42 12 August 2014 by Jacob Aron for New Scientist
A computer-verified proof of a 400-year-old problem could pave the way for a new era of mathematics, in which machines do the grunt work and leave humans free for deeper thinking.
The problem is a puzzle familiar to greengrocers everywhere: what is the best way to stack a collection of spherical objects, such as a display of oranges for sale? In 1611 Johannes Kepler suggested that a pyramid arrangement was the most efficient, but couldn't prove it.
Now, a mathematician has announced the completion of an epic quest to formally prove the so-called Kepler conjecture. "An enormous burden has been lifted from my shoulders," says Thomas Hales of the University of Pittsburgh, Pennsylvania, who led the work. "I suddenly feel ten years younger!"
Hales first presented a proof that Kepler's intuition was correct in 1998. Although there are infinite ways to stack infinitely many spheres, most are variations on only a few thousand themes. Hales broke the problem down into the thousands of possible sphere arrangements that mathematically represent the infinite possibilities, and used software to check them all.
But the proof was a 300-page monster that took 12 reviewers four years to check for errors. Even when it was published in the journal Annals of Mathematics in 2005, the reviewers could say only that they were "99 per cent certain" the proof was correct.
So in 2003, Hales started the Flyspeck project, an effort to vindicate his proof through formal verification. His team used two formal proof software assistants called Isabelle and HOL Light, both of which are built on a small kernel of logic that has been intensely scrutinised for any errors – this provides a foundation which ensures the computer can check any series of logical statements to confirm they are true.
On Sunday, the Flyspeck team announced they had finally translated the dense mathematics of Hale's proof into computerised form, and verified that it is indeed correct.
"This technology cuts the mathematical referees out of the verification process," says Hales. "Their opinion about the correctness of the proof no longer matters."
"It has been a huge effort," says Alan Bundy of the University of Edinburgh, UK, who was not involved in the work. He adds that he hopes Flyspeck's success will inspire other mathematicians to start using proof assistants. "A world-famous mathematician has turned his hand toward automated theorem proving, that kind of sociological fact is very important," he says. "This is a case study which could start to become the norm."
Ideally, proof assistants would work in the background as mathematicians puzzled through new ideas. Software can already prove some basic concepts by itself, but it could be easier to use. "We need some way of exploring the proof, getting a big picture," says Bundy. "To see everything in all the gory detail is just beyond us, as humans we can't absorb that much."
As for Hales, he's ready to move on. "I have a box full of ideas that I have set aside while working on this formal proof," he says. "Let's hope that the next project does not take 20 years!"
