×

A formal proof of the Kepler conjecture. (English) Zbl 1379.52018

Kepler’s conjecture says that the density of any packing of unit balls in Euclidean three space cannot be larger than \(\pi/\sqrt{18}\), the density of the face-centered cubic packing. The complex proof of that conjecture by T. C. Hales and S. P. Ferguson, published in [Discrete Comput. Geom. 36, No. 1, 5–20 (2006; Zbl 1186.52010); ibid. 36, No. 1, 21–69 (2006; Zbl 1186.52014); ibid. 36, No. 1, 71–110 (2006; Zbl 1186.52011); ibid. 36, No. 1, 205–265 (2006; Zbl 1186.52013); ibid. 36, No. 1, 111–166 (2006; Zbl 1186.52012); ibid. 36, No. 1, 167–204 (2006; Zbl 1186.52009)], has left the referees with some degree of incertitude concerning its correctness. Therefore Hales initiated the Flyspeck project of a formal proof of Kepler’s conjecture using the HOL Light and Isabelle proof assistants. The paper under review reports on that proof.

MSC:

52C17 Packing and covering in \(n\) dimensions (aspects of discrete geometry)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] M.Adams, ‘Introducing HOL Zero’, inMathematical Software-ICMS 2010 (Springer, 2010), 142-143.10.1007/978-3-642-15582-6_25
[2] M.Adams, ‘Flyspecking Flyspeck’, inMathematical Software-ICMS 2014 (Springer, 2014), 16-20. · Zbl 1403.68220
[3] M.Adams and D.Aspinall, ‘Recording and refactoring HOL Light tactic proofs’, inProceedings of the IJCAR Workshop on Automated Theory Exploration (2012).
[4] G.Bauer, ‘Formalizing plane graph theory – towards a formalized proof of the Kepler conjecture’. PhD Thesis, Technische Universität München, 2006. http://mediatum.ub.tum.de/doc/601794/document.pdf.
[5] G.Bauer and T.Nipkow, ‘Flyspeck I: Tame graphs’, inThe Archive of Formal Proofs (eds. G.Klein, T.Nipkow and L.Paulson) http://afp.sf.net/entries/Flyspeck-Tame.shtml, May 2006. Formal proof development. · Zbl 1222.52018
[6] L.Fejes Tóth, Lagerungen in der Ebene auf der Kugel und im Raum, 1st edn, (Springer, Berlin-New York, 1953). · Zbl 0052.18401
[7] Flyspeck, The Flyspeck Project, 2014. https://github.com/flyspeck/flyspeck.
[8] GLPK, GLPK (GNU Linear Programming Kit). http://www.gnu.org/software/glpk/.
[9] G.Gonthier, A.Asperti, J.Avigad, Y.Bertot, C.Cohen, F.Garillot, S.Le Roux, A.Mahboubi, R.O’Connor and S. O.Biha, ‘A machine-checked proof of the odd order theorem’, inInteractive Theorem Proving (Springer, 2013), 163-179.10.1007/978-3-642-39634-2_14 · Zbl 1317.68211
[10] M.Gordon, R.Milner and C.Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, 78 (1979).10.1007/3-540-09724-4 · Zbl 0421.68039
[11] M. J. C.Gordon and T. F.Melham, Introduction to HOL: a Theorem Proving Environment for Higher Order Logic (Cambridge University Press, 1993). · Zbl 0779.68007
[12] F.Haftmann and T.Nipkow, ‘Code generation via higher-order rewrite systems’, inFunctional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings (Springer, 2010), 103-117. https://dx.doi.org/10.1007/978-3-642-12251-4_9. · Zbl 1284.68131
[13] T.Hales, Developments in formal proofs. Bourbaki Seminar, 2013/2014 (1086):1086-1-23, 2014. · Zbl 1356.03003
[14] T. C.Hales, ‘A proof of the Kepler conjecture’, Ann. of Math. (2)162 (2005), 1063-1183.10.4007/annals.2005.162.1065 · Zbl 1096.52010 · doi:10.4007/annals.2005.162.1065
[15] T. C.Hales, ‘Introduction to the Flyspeck Project’, inMathematics, Algorithms, Proofs (eds. T.Coquand, H.Lombardi and M.-F.Roy) Dagstuhl Seminar Proceedings, Dagstuhl, Germany, number 05021 (Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2006), http://drops.dagstuhl.de/opus/volltexte/2006/432.
[16] T. C.Hales, ‘The strong dodecahedral conjecture and Fejes Tóth’s contact conjecture’, Technical Report, 2011.
[17] T. C.Hales, Dense Sphere Packings: a Blueprint for Formal Proofs, London Mathematical Society Lecture Note Series, 400 (Cambridge University Press, 2012).10.1017/CBO9781139193894 · Zbl 1263.52001 · doi:10.1017/CBO9781139193894
[18] T. C.Hales and S. P.Ferguson, ‘The Kepler conjecture’, Discrete Comput. Geom.36(1) (2006), 1-269.10.1007/s00454-005-1209-8 · Zbl 1186.52014
[19] T. C.Hales, J.Harrison, S.McLaughlin, T.Nipkow, S.Obua and R.Zumkeller, ‘A revision of the proof of the Kepler Conjecture’, Discrete Comput. Geom.44(1) (2010), 1-34.10.1007/s00454-009-9148-4 · Zbl 1195.52004
[20] J.Harrison, ‘Towards self-verification of HOL Light’, inAutomated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (eds. U.Furbach and N.Shankar) Lecture Notes in Computer Science, 4130 (Springer, 2006), 177-191. ISBN 3-540-37187-7. https://dx.doi.org/10.1007/11814771_17. · Zbl 1222.68364
[21] J.Harrison, ‘Without loss of generality’, inProceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009 (eds. S.Berghofer, T.Nipkow, C.Urban and M.Wenzel) Lecture Notes in Computer Science, 5674 (Springer, Munich, Germany, 2009), 43-59. · Zbl 1252.68254
[22] J.Harrison, ‘HOL Light: An overview’, inTheorem Proving in Higher Order Logics (Springer, 2009), 60-66.10.1007/978-3-642-03359-9_4 · Zbl 1252.68255
[23] J.Harrison, The HOL Light theorem prover, 2014. http://www.cl.cam.ac.uk/∼jrh13/hol-light/index.html.
[24] C.Kaliszyk and A.Krauss, ‘Scalable LCF-style proof translation’, inProc. of the 4th International Conference on Interactive Theorem Proving (ITP’13) (eds. S.Blazy, C.Paulin-Mohring and D.Pichardie) Lecture Notes in Computer Science, 7998 (Springer, 2013), 51-66.10.1007/978-3-642-39634-2_7 · Zbl 1317.68214
[25] C.Kaliszyk and J.Urban, ‘Learning-assisted automated reasoning with Flyspeck’, J. Automat. Reason.53(2) (2014), 173-213. https://dx.doi.org/10.1007/s10817-014-9303-3.10.1007/s10817-014-9303-3 · Zbl 1314.68283
[26] C.Kaliszyk and J.Urban, ‘Learning-assisted theorem proving with millions of lemmas’, J. Symbolic Comput.69(0) (2014), 109-128. ISSN 0747-7171. doi:10.1016/j.jsc.2014.09.032. URL http://www.sciencedirect.com/science/article/pii/S074771711400100X.10.1016/j.jsc.2014.09.032 · Zbl 1315.68220
[27] J.Kepler, Strena seu de nive sexangula (Gottfried. Tampach, Frankfurt, 1611).
[28] G.Klein, K.Elphinstone, G.Heiser, J.Andronick, D.Cock, P.Derrin, D.Elkaduwe, K.Engelhardt, R.Kolanski, M.Norrish, T.Sewell, H.Tuch and S.Winwood, ‘seL4: formal verification of an OS kernel’, inProc. 22nd ACM Symposium on Operating Systems Principles 2009 (eds. J. N.Matthews and T. E.Anderson) (ACM, 2009), 207-220.
[29] R.Kumar, R.Arthan, M. O.Myreen and S.Owens, ‘HOL with definitions: semantics, soundness, and a verified implementation’, inInteractive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (eds. G.Klein and R.Gamboa) Lecture Notes in Computer Science, 8558 (Springer, 2014), 308-324. ISBN 978-3-319-08969-0.https://dx.doi.org/10.1007/978-3-319-08970-6_20. · Zbl 1416.68167
[30] J.Lagarias, The Kepler Conjecture and its Proof (Springer, 2009), 3-26.
[31] X.Leroy, ‘Formal certification of a compiler back-end, or: programming a compiler with a proof assistant’, inACM SIGPLAN Notices41, (2006), 42-54. http://compcert.inria.fr/. · Zbl 1369.68124
[32] V.Magron, ‘Formal proofs for global optimization – templates and sums of squares’. PhD Thesis, École Polytechnique, 2013.
[33] C.Marchal, ‘Study of the Kepler’s conjecture: the problem of the closest packing’, Math. Z.267(3-4) (2011), 737-765. ISSN 0025-5874. https://dx.doi.org/10.1007/s00209-009-0644-2.10.1007/s00209-009-0644-2 · Zbl 1243.52017
[34] S.McLaughlin, ‘An interpretation of Isabelle/HOL in HOL Light’, inIJCAR (eds. U.Furbach and N.Shankar) Lecture Notes in Computer Science, 4130 (Springer, 2006), 192-204. · Zbl 1222.68370
[35] R. E.Moore, R. B.Kearfott and M. J.Cloud, Introduction to Interval Analysis (SIAM, 2009).10.1137/1.9780898717716 · Zbl 1168.65002
[36] T.Nipkow, ‘Verified efficient enumeration of plane graphs modulo isomorphism’, inInteractive Theorem Proving (ITP 2011) (eds. M.Van Eekelen, H.Geuvers, J.Schmaltz and F.Wiedijk) Lecture Notes in Computer Science, 6898 (Springer, 2011), 281-296.10.1007/978-3-642-22863-6_21 · Zbl 1342.68298
[37] T.Nipkow, L.Paulson and M.Wenzel, Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, 2283 (Springer, 2002), http://www.in.tum.de/∼nipkow/LNCS2283/. · Zbl 0994.68131
[38] T.Nipkow, G.Bauer and P.Schultz, ‘Flyspeck I: Tame graphs’, inAutomated Reasoning (IJCAR 2006) (eds. U.Furbach and N.Shankar) Lecture Notes in Computer Science, 4130 (Springer, 2006), 21-35.10.1007/11814771_4 · Zbl 1222.52018
[39] S.Obua, ‘Proving bounds for real linear programs in Isabelle/HOL’, inTheorem Proving in Higher Order Logics (eds. J.Hurd and T. F.Melham) Lecture Notes in Computer Science, 3603 (Springer, 2005), 227-244.10.1007/11541868_15 · Zbl 1152.68531
[40] S.Obua, ‘Flyspeck II: the basic linear programs’. PhD Thesis, Technische Universität München, 2008. · Zbl 1184.68465
[41] S.Obua and T.Nipkow, ‘Flyspeck II: the basic linear programs’, Ann. Math. Artif. Intell.56(3-4) (2009).10.1007/s10472-009-9168-z · Zbl 1184.68465
[42] S.Obua and S.Skalberg, ‘Importing HOL into Isabelle/HOL’, inAutomated Reasoning, Lecture Notes in Computer Science, 4130 (Springer, 2006), 298-302.10.1007/11814771_27
[43] A.Solovyev, ‘Formal methods and computations’. PhD Thesis, University of Pittsburgh, 2012. http://d-scholarship.pitt.edu/16721/.
[44] A.Solovyev and T. C.Hales, Efficient Formal Verification of Bounds of Linear Programs, Lecture Notes in Computer Science, 6824 (Springer, 2011), 123-132. · Zbl 1335.68238
[45] A.Solovyev and T. C.Hales, ‘Formal verification of nonlinear inequalities with Taylor interval approximations’, inNFM, Lecture Notes in Computer Science, 7871 (Springer, 2013), 383-397.
[46] O.Tange, ‘GNU parallel – the command-line power tool’, USENIX Mag.36(1) (2011), 42-47. URL http://www.gnu.org/s/parallel.
[47] C.Tankink, C.Kaliszyk, J.Urban and H.Geuvers, ‘Formal mathematics on display: A wiki for Flyspeck’, inMKM/Calculemus/DML (eds. J.Carette, D.Aspinall, C.Lange, P.Sojka and W.Windsteiger) Lecture Notes in Computer Science, 7961 (Springer, 2013), 152-167. ISBN 978-3-642-39319-8. · Zbl 1390.68751
[48] R.Zumkeller, ‘Global optimization in type theory’. PhD Thesis, École Polytechnique Paris, 2008.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.