Many elementary problems in geometry arise as part of the proof of the Kepler conjecture on sphere packings. In the original proof, most of these problems were solved by hand. This article investigates the methods that were used in the original proof and describes a number of other methods that might be used to automate the proofs of these problems. A companion article presents the collection of elementary problems in geometry for which automated proofs are sought. This article is a contribution to the Flyspeck project, which aims to give a complete formal proof of the Kepler conjecture.

In 1998, the oldest problem in discrete geometry, the 400-year old Kep ler conjecture, was solved. The conjecture asserts that the familiar cannonball packing of balls achieves the greatest density of any possible packing. The proof of the conjecture was unusually long, requiring nearly 300 pages of careful reasoning, 3 gigabytes of stored data, and 40,000 lines of specialized computer code. The computer verifications required for the proof were carried out over a period of years.