A FORMAL PROOF OF THE KEPLER CONJECTURE | Forum of Mathematics, Pi | Cambridge Core

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.

Adams, M., ‘Introducing HOL Zero’, inMathematical Software–ICMS 2010 (Springer, 2010), 142–143.Google Scholar

Adams, M., ‘Flyspecking Flyspeck’, inMathematical Software–ICMS 2014 (Springer, 2014), 16–20.CrossRefGoogle Scholar

Adams, M. and Aspinall, D., ‘Recording and refactoring HOL Light tactic proofs’, inProceedings of the IJCAR Workshop on Automated Theory Exploration (2012).Google Scholar

Fejes Tóth, L., Lagerungen in der Ebene auf der Kugel und im Raum, 1st edn, (Springer, Berlin–New York, 1953).CrossRefGoogle Scholar

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.Google Scholar

Gordon, M., Milner, R. and Wadsworth, C., Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, 78 (1979).CrossRefGoogle Scholar

Gordon, M. J. C. and Melham, T. F., Introduction to HOL: a Theorem Proving Environment for Higher Order Logic (Cambridge University Press, 1993).Google Scholar

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.Google Scholar

Hales, T., Developments in formal proofs. Bourbaki Seminar, 2013/2014 (1086):1086-1-23, 2014.Google Scholar

Hales, T. C., ‘A proof of the Kepler conjecture’, Ann. of Math. (2) 162 (2005), 1063–1183.Google Scholar

Hales, T. C., ‘Introduction to the Flyspeck Project’, inMathematics, Algorithms, Proofs (eds. Coquand, T., Lombardi, H. and Roy, M.-F.) 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.Google Scholar

Hales, T. C., ‘The strong dodecahedral conjecture and Fejes Tóth’s contact conjecture’, Technical Report, 2011.Google Scholar

Hales, T. C., Dense Sphere Packings: a Blueprint for Formal Proofs, London Mathematical Society Lecture Note Series, 400 (Cambridge University Press, 2012).Google Scholar

Hales, T. C. and Ferguson, S. P., ‘The Kepler conjecture’, Discrete Comput. Geom. 36(1) (2006), 1–269.Google Scholar

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.Google Scholar

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.) Lecture Notes in Computer Science, 4130 (Springer, 2006), 177–191. ISBN 3-540-37187-7. https://dx.doi.org/10.1007/11814771_17.Google Scholar

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.) Lecture Notes in Computer Science, 5674 (Springer, Munich, Germany, 2009), 43–59.Google Scholar

Harrison, J., ‘HOL Light: An overview’, inTheorem Proving in Higher Order Logics (Springer, 2009), 60–66.CrossRefGoogle Scholar

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.) Lecture Notes in Computer Science, 7998 (Springer, 2013), 51–66.CrossRefGoogle Scholar

Kepler, J., Strena seu de nive sexangula (Gottfried. Tampach, Frankfurt, 1611).Google Scholar

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.Google Scholar

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.) 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.Google Scholar

Lagarias, J., The Kepler Conjecture and its Proof (Springer, 2009), 3–26.Google Scholar

Magron, V., ‘Formal proofs for global optimization – templates and sums of squares’. PhD Thesis, École Polytechnique, 2013.Google Scholar

McLaughlin, S., ‘An interpretation of Isabelle/HOL in HOL Light’, inIJCAR (eds. Furbach, U. and Shankar, N.) Lecture Notes in Computer Science, 4130 (Springer, 2006), 192–204.Google Scholar

Moore, R. E., Kearfott, R. B. and Cloud, M. J., Introduction to Interval Analysis (SIAM, 2009).Google Scholar

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.) Lecture Notes in Computer Science, 6898 (Springer, 2011), 281–296.Google Scholar

Nipkow, T., Bauer, G. and Schultz, P., ‘Flyspeck I: Tame graphs’, inAutomated Reasoning (IJCAR 2006) (eds. Furbach, U. and Shankar, N.) Lecture Notes in Computer Science, 4130 (Springer, 2006), 21–35.Google Scholar

Obua, S., ‘Proving bounds for real linear programs in Isabelle/HOL’, inTheorem Proving in Higher Order Logics (eds. Hurd, J. and Melham, T. F.) Lecture Notes in Computer Science, 3603 (Springer, 2005), 227–244.CrossRefGoogle Scholar

Obua, S., ‘Flyspeck II: the basic linear programs’. PhD Thesis, Technische Universität München, 2008.Google Scholar

Obua, S. and Nipkow, T., ‘Flyspeck II: the basic linear programs’, Ann. Math. Artif. Intell. 56(3–4) (2009).Google Scholar

Obua, S. and Skalberg, S., ‘Importing HOL into Isabelle/HOL’, inAutomated Reasoning, Lecture Notes in Computer Science, 4130 (Springer, 2006), 298–302.Google Scholar

Solovyev, A. and Hales, T. C., Efficient Formal Verification of Bounds of Linear Programs, Lecture Notes in Computer Science, 6824 (Springer, 2011), 123–132.Google Scholar

Solovyev, A. and Hales, T. C., ‘Formal verification of nonlinear inequalities with Taylor interval approximations’, inNFM, Lecture Notes in Computer Science, 7871 (Springer, 2013), 383–397.Google Scholar

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.) Lecture Notes in Computer Science, 7961 (Springer, 2013), 152–167. ISBN 978-3-642-39319-8.Google Scholar

Zumkeller, R., ‘Global optimization in type theory’. PhD Thesis, École Polytechnique Paris, 2008.Google Scholar