COMPUTER PROOF AND THE A PRIORI

Burge’s paper focuses on the four color theorem as the standard case of so-called ‘computer proof‘. There is a more recent case, with an even cooler name: the Sphere Packing Conjecture:

Following the approach suggested by Fejes Tóth, Thomas Hales, then at the University of Michigan, determined that the maximum density of all arrangements could be found by minimising a function with 150 variables. In 1992, assisted by his graduate student Samuel Ferguson, he embarked on a research programme to systematically apply linear programming methods to find a lower bound on the value of this function for each one of a set of over 5,000 different configurations of spheres. If a lower bound could be found for every one of these configurations that was greater than the value for the cubic close packing arrangement, then the Kepler conjecture would be proved. To find lower bounds for all cases involved solving around 100,000 linear programming problems.

When presenting the progress of his project in 1996, Hales said that the end was in sight, but it might take “a year or two” to complete. In August 1998 Hales announced that the proof was complete. At that stage it consisted of 250 pages of notes and 3 gigabytes of computer programs, data and results.

Despite the unusual nature of the proof, the editors of the Annals of Mathematics agreed to publish it, provided it was accepted by a panel of twelve referees. In 2003, after four years of work, the head of the referee’s panel Gábor Fejes Tóth (son of László Fejes Tóth) reported that the panel were “99% certain” of the correctness of the proof, but they could not certify the correctness of all of the computer calculations.

In February 2003 Hales published a 100-page paper (PDF) describing the non-computer part of his proof in detail.