Some Algorithms Arising in the Proof of the Kepler Conjecture
By any account, the 1998 proof of the Kepler conjecture is complex. The thesis underlying this article is that the proof is complex because it is highly under-automated. Throughout that proof, manual procedures are used where automated ones would have bee
- PDF / 376,311 Bytes
- 19 Pages / 439 x 666 pts Page_size
- 8 Downloads / 208 Views
Abstract By any account, the 1998 proof of the Kepler conjecture is complex. The thesis underlying this article is that the proof is complex because it is highly under-automated. Throughout that proof, manual procedures are used where automated ones would have been better suited. This paper gives a series of nonlinear optimization algorithms and shows how a systematic application of these algorithms would bring substantial simplifications to the original proof.
1
Introduction
In 1998 a proof of the Kepler conjecture was completed [8]. By any account, that solution is complex (300 pages of text, 3 GB stored data on the computer, computer calculations taking months, 40K lines of computer code, and so forth). The thesis underlying this article is that the 1998 proof is complex because it is highly under-automated. Throughout that proof, manual procedures are used where automated ones would have been better suited. Ultimately, a properly automated proof of the Kepler conjecture might be short and elegant. The hope is that the Kepler conjecture might eventually become an instance of a general family of optimization problems for which general optimization techniques exist. Just as today linear programming problems of a moderate size can be solved without fanfare, we might hope that problems of a moderate size in this family might be routinely solved by general algorithms. The proof of the Kepler conjecture would then consist of demonstrating that the Kepler conjecture can be structured as a problem in this family, and then invoking the general algorithm to solve the problem. As a step toward that objective, this article frames the primary algorithms of that proof in sufficient generality that they may be applied to much larger families of problems. The algorithms are arranged into four sections: Quantifier Elimination, Linear Assembly Problems, Automated Inequality Proving, Plane Graph Generation. B. Aronov et al. (eds.), Discrete and Computational Geometry © Springer-Verlag Berlin Heidelberg 2003
490
T.C. Hales
We do not claim any originality in the algorithms. In fact, the purpose is just the contrary: to exhibit the proof of the Kepler conjecture insofar as possible as an instance of standard optimization techniques. To keep things as general as possible, the algorithms we present here will make no mention of the particulars of the Kepler conjecture. A final section lists parts of the 1998 proof that can be structured according to these general algorithms.
2
Quantifier Elimination
We might try to structure the Kepler conjecture as a statement in the elementary theory of the real numbers. Tarski proved the decidability of this theory, through quantifier elimination. G. Collins and others have developed and implemented concrete algorithms to perform quantifier elimination [5]. The Kepler conjecture, as formulated in [6], is not a statement in this theory, because the transcendental arctangent function enters into the statement. However, it seems that the arctangent is not essential to the formulation of the Kepler con
Data Loading...
