The Kepler conjecture<\/a> is the assertion that the simple scheme of stacking oranges typically seen in a supermarket has the highest possible average density, namely pi\/(3 sqrt(2)) = 0.740480489…, for any possible arrangement, regular or irregular. It is named after 17th-century astronomer Johannes Kepler, who first proposed that planets orbited in elliptical paths around the sun.<\/p>\n Optimal stacking of oranges.<\/p><\/div>\n In the early 1990s, Thomas Hales, following an approach first suggested by Laszlo Fejes Toth<\/a> in 1953, determined that the maximum density of all possible arrangements could be obtained by minimizing a certain function with 150 variables. In 1992, assisted by his graduate student Samuel Ferguson (son of famed mathematician-sculptor Helaman Ferguson<\/a>), Hales embarked on a multi-year effort to find a lower bound for the function for each of roughly 5000 different configurations of spheres, using a linear programming approach. In 1998, Hales and Ferguson announced that their project was complete, documented by 250 pages of notes and three Gbyte of computer code, data and results. Three Gbyte may seem like a lot but in the current world of big data it no longer is. We have recently put a 108 Gbyte image of Pi<\/a> on line.<\/p>\n Hales’ proof, when submitted to the prestigious journal Annals of Mathematics<\/a>, was met with some controversy. The journal submitted the manuscript to a panel of twelve referees, headed by Gabor Fejes Toth<\/a>, son of Lazlo Fejes Toth. In 2003, the panel reported that it was “99% certain” that the proof was sound, but that they could not verify the correctness of all of the computer calculations (which used non-certifiable numerics). The Annals<\/i> decided to publish the paper, initially accompanied with a caveat, but in the end omitted the caveat.<\/p>\n Given the chilly reception of Hales’ proof, he decided to embark on a collaborative effort to certify the proof via automated proof-checking (formal method) software. This project, named Flyspeck<\/a>, was begun in 2003, employing a combination of Isabelle<\/i> and HOL Light<\/i> formal proof assistants. Hales estimated that it would take 20 years to complete.<\/p>\n On 10 August 2014, Hales announced that the project was complete. Hales observed<\/a>,<\/p>\n This technology cuts the mathematical referees out of the verification process. … Their opinion about the correctness of the proof no longer matters.<\/p><\/blockquote>\n Perhaps, but we should add the caution<\/a> that this all assumes a correct level of of formalization and even that the output faithfully reproduces what the program actually did. In any event this a signal achievement.<\/p>\n![\"Optimal](\"http:\/\/upload.wikimedia.org\/wikipedia\/commons\/a\/a2\/HCP_Oranges.jpg\")
<\/a>Hales’ 2003 proof<\/h4>\n
The Flyspeck project<\/h4>\n