Kepler猜想证明中的一些算法
Some algorithms arising in the proof of the Kepler conjecture
摘要：
无论如何，1998年开普勒猜想的证明是复杂的。本文的论点是，证明是复杂的，因为它是高度自动化的。在整个证明过程中，在自动化程序更适合的地方使用手动程序。本文给出了一系列的非线性最优化算法，并展示了如何系统地应用这些算法将带来实质性的简化原来的证明。本文包括量词消除，线性组装问题，自动不等式证明，和平面图的离散几何的背景下产生的讨论。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
