开普勒猜想的形式化证明：批判性回顾
度量几何
2024-02-14 v1
摘要
开普勒猜想断言，在三维欧几里得空间中，任何全等球体的堆积密度均不超过面心立方堆积的密度。1998 年，Sam Ferguson 和我宣布了对该猜想的计算机辅助证明。审稿过程的长期延误促使我们启动了一个形式化证明开普勒猜想的项目，该项目于 2014 年在一项大型协作努力下完成。本文对该项目进行了批判性的重新评估。
引用
@article{arxiv.2402.08032,
title = {The Formal Proof of the Kepler Conjecture: a critical retrospective},
author = {Thomas Hales},
journal= {arXiv preprint arXiv:2402.08032},
year = {2024}
}
备注
14 pages. This article was written in 2020 for the book "Proof Assistants and Their Applications in Mathematics and Computer Science"