开普勒猜想的形式化证明：一项批判性回顾
The Formal Proof of the Kepler Conjecture: a critical retrospective
AI总结：
本文批判性回顾了开普勒猜想形式化证明项目，该项目源于1998年计算机辅助证明审稿延误，最终于2014年通过大规模合作完成。
摘要：
开普勒猜想断言，三维欧几里得空间中没有任何全等球体堆积的密度能超过面心立方堆积的密度。1998年，Sam Ferguson和我宣布了该猜想的计算机辅助证明。审稿过程的长期延误引发了一个为开普勒猜想提供形式化证明的项目，该项目于2014年通过大规模合作完成。本文对该项目进行了批判性重新评估。
英文摘要：
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. In 1998, Sam Ferguson and I announced a computer-assisted proof of this conjecture. Long delays in the refereeing process sparked a project to give a formal proof of the Kepler conjecture, which was completed in a large collaborative effort in 2014. This article gives a critical reappraisal of that project.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
