Some algorithms arising in the proof of the Kepler conjecture

Simple item page
dc.creatorHales, Thomas C.
dc.date2002-05-19
dc.date.accessioned2026-07-07T04:48:36Z
dc.date.available2026-07-07T04:48:36Z
dc.descriptionBy 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.
dc.description14 pages, 5 figures
dc.identifierhttps://arxiv.org/abs/math/0205209
dc.identifierhttp://arxiv.org/abs/math/0205209
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/64108
dc.subjectMetric Geometry
dc.subjectOptimization and Control
dc.titleSome algorithms arising in the proof of the Kepler conjecture
dc.typetext

Files

Collections

arXiv