In 1611, the German mathematician, astronomer, and astrologer Johannes Kepler presented a mathematical conjecture about sphere packing in 3-dimensional Euclidean space. This intriguing problem has perplexed mathematicians for almost 400 years, until Thomas Callister Hales presented a computer-aided solution in 1998.
According to Kepler, “no arrangement of equally sized spheres filling space has a greater average density than that of the cubic close packing and hexagonal close packing arrangements.” In simpler words, Kepler’s conjecture means that the standard manner of packing unit spheres is the densest. Instead of packing oranges in one layer on the top of another, identical one, Kepler realized that greengrocers used the space more efficiently by positioning the oranges in the hollows made by the oranges on the lower level (the formal term for this type of arrangement is face-centered cubic lattice). According to this method,
which is the highest average density that can be achieved when arranging spheres. The Kepler problem is finding the densest (not necessarily periodic) sphere packing.
This proportion seems obvious to all common people, but mathematicians could not prove it. The problem has intrigued and stymied many genius mathematicians over four centuries, including R. Buckminster Fuller, David Hilbert, and C.F. Gauss. Buckminster Fuller, an American neo-futurist architect, claimed to have a proof in 1975, but presented a mere description of face-centered cubic packing, without offering a proof for this optimum.
Wu-Yi Hsiang (1993, 2001), was another mathematician who claimed to have a proof for the Kepler conjecture. He used geometric methods to present the journey from the problem to the solution, but did not provide acceptable proof for the key statements. Hsiang’s method sparked many controversies in the mathematics community, so the members of the jury had to be very careful with the following proofs they deliberated.
In 1998, Thomas Callister Hales announced that the Kepler conjecture could be proved through extensive use of computer calculations. After that, Hales completed a proof published in a series of papers. Hales’ proof relies on methods from the theory of global optimization, interval arithmetics, and linear programming. A jury of twelve referees started deliberating the proof in 1998, and gave up after years of effort. Although the reviewers were 99% certain that the proof was correct, in 2003 they reported that parts of Hales’ paper were not possible to check.
In an attempt to verify the proof and offer a clearer manuscript, Thomas Hales started the “Flyspeck project”, which had the goal to verify each step by automatic proof checking software. According to his own estimations, producing a complete formal proof would require 20 years of work. However, the Flyspeck project was announced completed on August 10, 2014. The formal proof has the same general approach as the proof that was originally published in 1997, but has modifications in the geometric partition of space. Finally, all greengrocers around the world can be sure that they arrange oranges in the most efficient, mathematically proven, method.
