A FORMAL PROOF OF THE KEPLER CONJECTURE
A FORMAL PROOF OF THE KEPLER CONJECTURE
复制标题
DOI：
10.1017/fmp.2017.1
复制
发表时间：
2017-05-29
影响因子：
2.3
通讯作者：
Zumkeller, Roland
中科院分区：
文献类型：
--
作者：
Hales, Thomas;Adams, Mark;Zumkeller, Roland
本文描述了在HOL Light和Isabelle证明助手的组合中，稠密球包装上开普勒猜想的一个形式证明。这篇论文构成了现已完成的苍蝇计划的官方出版记述。
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.