Computer software verifies mathematical fruit-stacking proof

New Scientist : Finding the best way to stack oranges or other spherical fruit has perplexed grocers for centuries. Four hundred years ago Johannes Kepler proposed a pyramid shape, but couldn’t prove it mathematically. In 1998 mathematician Thomas Hales devised a proof so complex it took 12 reviewers four years to check. Even then they were not 100% certain. So Hales initiated the Flyspeck project —a method of using a computer to check a mathematical proof. With the use of two so-called formal proof software assistants—Isabelle and HOL Light—Hales’s team verified the proof by translating the mathematics into computerized form and letting the computer do the bulk of the calculations. Hales hopes that such formal proofs will not only speed up the process but also provide a much higher degree of certification than is possible with human peer review.