A FORMAL PROOF OF THE KEPLER CONJECTURE

被引：241

作者：

Hales, Thomas ^{[1
]}

Adams, Mark ^{[2
,3
]}

Bauer, Gertrud ^{[4
]}

Tat Dat Dang ^{[5
]}

Harrison, John ^{[6
]}

Le Truong Hoang ^{[7
]}

Kaliszyk, Cezary ^{[8
]}

Magron, Victor ^{[9
]}

Mclaughlin, Sean ^{[10
]}

Tat Thang Nguyen ^{[7
]}

Quang Truong Nguyen ^{[1
]}

Nipkow, Tobias ^{[11
]}

Obua, Steven ^{[12
]}

Pleso, Joseph ^{[13
]}

Rute, Jason ^{[14
]}

Solovyev, Alexey ^{[15
]}

Thi Hoai An Ta ^{[7
]}

Nam Trung Tran ^{[7
]}

Thi Diep Trieu ^{[16
]}

Urban, Josef ^{[17
]}

Vu, Ky ^{[18
]}

Zumkeller, Roland ^{[18
]}

机构：

[1] Univ Pittsburgh, Pittsburgh, PA 15260 USA

[2] Proof Technol Ltd, Worcester, England

[3] Radboud Univ Nijmegen, Nijmegen, Netherlands

[4] ESG Elekt Syst & Logist GmbH, Berlin, Germany

[5] CanberraWeb, 5-47-49 Vicars St, Mitchell, ACT 2911, Australia

[6] Intel Corp, Santa Clara, CA 95051 USA

[7] Vietnam Acad Sci & Technol, Inst Math, Hanoi, Vietnam

[8] Univ Innsbruck, Innsbruck, Austria

[9] CNRS VERIMAG, Grenoble, France

[10] Amazon, Seattle, WA USA

[11] Tech Univ Munich, Munich, Germany

[12] Univ Edinburgh, Edinburgh, Midlothian, Scotland

[13] Philips Elect North Amer Corp, Andover, MA USA

[14] Penn State Univ, University Pk, PA 16802 USA

[15] Univ Utah, Salt Lake City, UT 84112 USA

[16] AXA China Reg Insurance Co Ltd, Hong Kong, Hong Kong, Peoples R China

[17] CIIRC, Prague, Czech Republic

[18] Chinese Univ Hong Kong, Hong Kong, Hong Kong, Peoples R China

来源：

FORUM OF MATHEMATICS PI | 2017年 / 5卷

基金：

美国国家科学基金会;

关键词：

HOL;

D O I：

10.1017/fmp.2017.1

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

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.

引用

页数：29

共 48 条

[1]

Adams Mark, 2014, Mathematical Software - ICMS 2014. 4th International Congress. Proceedings. LNCS: 8592, P16, DOI 10.1007/978-3-662-44199-2_3

[2]

Adams M., 2012, P IJCAR WORKSH AUT T

[3]

Adams M, 2010, LECT NOTES COMPUT SC, V6327, P142, DOI 10.1007/978-3-642-15582-6_25

[4]

[Anonymous], 2014, ITP

[5]

[Anonymous], 2006, MATH ALGORITHMS PROO

[6]

[Anonymous], 2012, London Math Soc. Lecture Note Series

[7]

[Anonymous], 1979, LECT NOTES COMPUTER

[8]

[Anonymous], 2014, THE FLYSPECK PROJECT

[9]

[Anonymous], The USENIX Magazine, V36 36, P42, DOI DOI 10.5281/ZENODO.16303

[10]

Bauer G., 2006, THESIS

← 1 2 3 4 5 →