2002/05/19 by Thomas C. Hales, Hales, Thomas C.
Mathematics · #FOS: Mathematics #Metric Geometry (math.MG) #Optimization and Control (math.OC) #math.MG #math.OC
paper · pdf · doi:10.48550/arxiv.math/0205209
14 pages, 5 figures
arxiv created 2002/05/19 · arxiv updated 2009/11/30
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.