zbMATH — the first resource for mathematics

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.

52C17 Packing and covering in \(n\) dimensions (aspects of discrete geometry)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Adams, M., ‘Introducing HOL Zero’, inMathematical Software-ICMS 2010 (Springer, 2010), 142-143. doi:10.1007/978-3-642-15582-6_25
[2] Adams, M., ‘Flyspecking Flyspeck’, inMathematical Software-ICMS 2014 (Springer, 2014), 16-20. · Zbl 1403.68220
[3] Adams, M. and Aspinall, D., ‘Recording and refactoring HOL Light tactic proofs’, inProceedings of the IJCAR Workshop on Automated Theory Exploration (2012).
[4] Bauer, G., ‘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] Bauer, G. and Nipkow, T., ‘Flyspeck I: Tame graphs’, inThe Archive of Formal Proofs (eds. Klein, G., Nipkow, T. and Paulson, L.) http://afp.sf.net/entries/Flyspeck-Tame.shtml, May 2006. Formal proof development. · Zbl 1222.52018
[6] Fejes Tóth, L., Lagerungen in der Ebene auf der Kugel und im Raum, (1953), Springer: Springer, Berlin-New York · Zbl 0052.18401
[7] , The Flyspeck Project, 2014. https://github.com/flyspeck/flyspeck.
[8] , GLPK (GNU Linear Programming Kit). http://www.gnu.org/software/glpk/.
[9] Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R. and Biha, S. O.et al., ‘A machine-checked proof of the odd order theorem’, inInteractive Theorem Proving (Springer, 2013), 163-179. doi:10.1007/978-3-642-39634-2_14 · Zbl 1317.68211
[10] Gordon, M., Milner, R. and Wadsworth, C., Edinburgh LCF: A Mechanized Logic of Computation, (1979). doi:10.1007/3-540-09724-4
[11] Gordon, M. J. C. and Melham, T. F., Introduction to HOL: a Theorem Proving Environment for Higher Order Logic (Cambridge University Press, 1993). · Zbl 0779.68007
[12] Haftmann, F. and Nipkow, T., ‘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] Hales, T., Developments in formal proofs. Bourbaki Seminar, 2013/2014 (1086):1086-1-23, 2014.
[14] Hales, T. C., A proof of the Kepler conjecture, Ann. of Math. (2), 162, 1063-1183, (2005) · Zbl 1096.52010
[15] Hales, T. C., ‘Introduction to the Flyspeck Project’, inMathematics, Algorithms, Proofs (eds. Coquand, T., Lombardi, H. and Roy, M.-F.) (Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany, 2006), http://drops.dagstuhl.de/opus/volltexte/2006/432.
[16] Hales, T. C., ‘The strong dodecahedral conjecture and Fejes Tóth’s contact conjecture’, Technical Report, 2011.
[17] Hales, T. C., Dense Sphere Packings: a Blueprint for Formal Proofs, (2012), Cambridge University Press · Zbl 1263.52001
[18] Hales, T. C. and Ferguson, S. P., ‘The Kepler conjecture’, Discrete Comput. Geom.36(1) (2006), 1-269. doi:10.1007/s00454-005-1209-8 · Zbl 1186.52014
[19] Hales, T. C., Harrison, J., Mclaughlin, S., Nipkow, T., Obua, S. and Zumkeller, R., ‘A revision of the proof of the Kepler Conjecture’, Discrete Comput. Geom.44(1) (2010), 1-34. doi:10.1007/s00454-009-9148-4 · Zbl 1195.52004
[20] Harrison, J., ‘Towards self-verification of HOL Light’, inAutomated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (eds. Furbach, U. and Shankar, N.) (Springer, 2006), 177-191. ISBN 3-540-37187-7. https://dx.doi.org/10.1007/11814771_17. · Zbl 1222.68364
[21] Harrison, J., ‘Without loss of generality’, inProceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009 (eds. Berghofer, S., Nipkow, T., Urban, C. and Wenzel, M.) (Springer, Munich, Germany, 2009), 43-59. · Zbl 1252.68254
[22] Harrison, J., ‘HOL Light: An overview’, inTheorem Proving in Higher Order Logics (Springer, 2009), 60-66. doi:10.1007/978-3-642-03359-9_4 · Zbl 1252.68255
[23] Harrison, J., The HOL Light theorem prover, 2014. http://www.cl.cam.ac.uk/∼jrh13/hol-light/index.html.
[24] Kaliszyk, C. and Krauss, A., ‘Scalable LCF-style proof translation’, inProc. of the 4th International Conference on Interactive Theorem Proving (ITP’13) (eds. Blazy, S., Paulin-Mohring, C. and Pichardie, D.) (Springer, 2013), 51-66. doi:10.1007/978-3-642-39634-2_7 · Zbl 1317.68214
[25] Kaliszyk, C. and Urban, J., ‘Learning-assisted automated reasoning with Flyspeck’, J. Automat. Reason.53(2) (2014), 173-213. https://dx.doi.org/10.1007/s10817-014-9303-3. doi:10.1007/s10817-014-9303-3 · Zbl 1314.68283
[26] Kaliszyk, C. and Urban, J., ‘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. doi:10.1016/j.jsc.2014.09.032 · Zbl 1315.68220
[27] Kepler, J., Strena seu de nive sexangula, (1611), Gottfried. Tampach: Gottfried. Tampach, Frankfurt
[28] Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H. and Winwood, S., ‘seL4: formal verification of an OS kernel’, inProc. 22nd ACM Symposium on Operating Systems Principles 2009 (eds. Matthews, J. N. and Anderson, T. E.) (ACM, 2009), 207-220.
[29] Kumar, R., Arthan, R., Myreen, M. O. and Owens, S., ‘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. Klein, G. and Gamboa, R.) (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] Lagarias, J., The Kepler Conjecture and its Proof, 3-26, (2009), Springer
[31] Leroy, X., ‘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] Magron, V., ‘Formal proofs for global optimization – templates and sums of squares’. PhD Thesis, École Polytechnique, 2013.
[33] Marchal, C., ‘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. doi:10.1007/s00209-009-0644-2 · Zbl 1243.52017
[34] Mclaughlin, S., ‘An interpretation of Isabelle/HOL in HOL Light’, inIJCAR (eds. Furbach, U. and Shankar, N.) (Springer, 2006), 192-204. · Zbl 1222.68370
[35] Moore, R. E., Kearfott, R. B. and Cloud, M. J., Introduction to Interval Analysis (SIAM, 2009). doi:10.1137/1.9780898717716 · Zbl 1168.65002
[36] Nipkow, T., ‘Verified efficient enumeration of plane graphs modulo isomorphism’, inInteractive Theorem Proving (ITP 2011) (eds. Van Eekelen, M., Geuvers, H., Schmaltz, J. and Wiedijk, F.) (Springer, 2011), 281-296. doi:10.1007/978-3-642-22863-6_21 · Zbl 1342.68298
[37] Nipkow, T., Paulson, L. and Wenzel, M., Isabelle/HOL - A Proof Assistant for Higher-Order Logic, (Springer, 2002), http://www.in.tum.de/∼nipkow/LNCS2283/. · Zbl 0994.68131
[38] Nipkow, T., Bauer, G. and Schultz, P., ‘Flyspeck I: Tame graphs’, inAutomated Reasoning (IJCAR 2006) (eds. Furbach, U. and Shankar, N.) (Springer, 2006), 21-35. doi:10.1007/11814771_4 · Zbl 1222.52018
[39] Obua, S., ‘Proving bounds for real linear programs in Isabelle/HOL’, inTheorem Proving in Higher Order Logics (eds. Hurd, J. and Melham, T. F.) (Springer, 2005), 227-244. doi:10.1007/11541868_15 · Zbl 1152.68531
[40] Obua, S., ‘Flyspeck II: the basic linear programs’. PhD Thesis, Technische Universität München, 2008. · Zbl 1184.68465
[41] Obua, S. and Nipkow, T., ‘Flyspeck II: the basic linear programs’, Ann. Math. Artif. Intell.56(3-4) (2009). doi:10.1007/s10472-009-9168-z · Zbl 1184.68465
[42] Obua, S. and Skalberg, S., ‘Importing HOL into Isabelle/HOL’, inAutomated Reasoning, (Springer, 2006), 298-302. doi:10.1007/11814771_27
[43] Solovyev, A., ‘Formal methods and computations’. PhD Thesis, University of Pittsburgh, 2012. http://d-scholarship.pitt.edu/16721/.
[44] Solovyev, A. and Hales, T. C., Efficient Formal Verification of Bounds of Linear Programs, (Springer, 2011), 123-132. · Zbl 1335.68238
[45] Solovyev, A. and Hales, T. C., ‘Formal verification of nonlinear inequalities with Taylor interval approximations’, inNFM, (Springer, 2013), 383-397.
[46] Tange, O., ‘GNU parallel – the command-line power tool’, USENIX Mag.36(1) (2011), 42-47. URL http://www.gnu.org/s/parallel.
[47] Tankink, C., Kaliszyk, C., Urban, J. and Geuvers, H., ‘Formal mathematics on display: A wiki for Flyspeck’, inMKM/Calculemus/DML (eds. Carette, J., Aspinall, D., Lange, C., Sojka, P. and Windsteiger, W.) (Springer, 2013), 152-167. ISBN 978-3-642-39319-8. · Zbl 1390.68751
[48] Zumkeller, R., ‘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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.