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鈥檛 prove it.
Now, a mathematician has announced the completion of an epic quest to formally prove the so-called . 鈥淎n enormous burden has been lifted from my shoulders,鈥� says of the University of Pittsburgh, Pennsylvania, who led the work. 鈥淚 suddenly feel ten years younger!鈥�
Advertisement
Hales first presented a proof that Kepler鈥檚 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 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鈥檚 proof into computerised form, and verified that it is indeed correct.
鈥淭his technology cuts the mathematical referees out of the verification process,鈥� says Hales. 鈥淭heir opinion about the correctness of the proof no longer matters.鈥�
鈥淚t has been a huge effort,鈥� says of the University of Edinburgh, UK, who was not involved in the work. He adds that he hopes Flyspeck鈥檚 success will inspire other mathematicians to start using proof assistants. 鈥淎 world-famous mathematician has turned his hand toward automated theorem proving, that kind of sociological fact is very important,鈥� he says. 鈥淭his 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. 鈥淲e need some way of exploring the proof, getting a big picture,鈥� says Bundy. 鈥淭o see everything in all the gory detail is just beyond us, as humans we can鈥檛 absorb that much.鈥�
As for Hales, he鈥檚 ready to move on. 鈥淚 have a box full of ideas that I have set aside while working on this formal proof,鈥� he says. 鈥淟et鈥檚 hope that the next project does not take 20 years!鈥�
