arXiv · math/0205209
Some algorithms arising in the proof of the Kepler conjecture
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 article gives a series of nonlinear optimization algorithms and shows how a systematic application of these algorithms would bring substantial simplifications to the original proof. This article includes a discussion of quantifier elimination, linear assembly problems, automated inequality proving, and plane graph generation in the context of discrete geometry.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Thomas C. Hales. 2002-05-19. Some algorithms arising in the proof of the Kepler conjecture. https://arxiv.org/abs/math/0205209
Cite the original work for its findings. Save a collection to share your selection of sources.