Introduction
On 10 August 2014, a team led by Thomas Hales of the University of Pittsburgh, USA, announced that their decade-long effort to construct a computer-verified formal proof of the Kepler conjecture was now complete. The project was known as Flyspeck, a rough acronym for “Formal Proof of Kepler.”
The Kepler conjecture 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.
Optimal stacking of oranges.
Hales’ 2003 proof
In the early 1990s, Thomas Hales, following an approach first suggested by Laszlo Fejes Toth 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), 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 on line.
Hales’ proof, when submitted to the prestigious journal Annals of Mathematics, was met with some controversy. The journal submitted the manuscript to a panel of twelve referees, headed by Gabor Fejes Toth, 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 decided to publish the paper, initially accompanied with a caveat, but in the end omitted the caveat.
The Flyspeck project
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, was begun in 2003, employing a combination of Isabelle and HOL Light formal proof assistants. Hales estimated that it would take 20 years to complete.
On 10 August 2014, Hales announced that the project was complete. Hales observed,
This technology cuts the mathematical referees out of the verification process. … Their opinion about the correctness of the proof no longer matters.
Perhaps, but we should add the caution 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.
Alan Bundy of the University of Edinburgh commented that Hales’ use of automated proof assistants might be seen as a significant milestone in the field of research mathematics:
A world-famous mathematician has turned his hand toward automated theorem proving; that kind of sociological fact is very important. … This is a case study which could start to become the norm.
In the meantime, we can shop at the supermarket confident that oranges are being stacked in the most efficient way possible! And we may have some fine new formal inequality provers.