Hostname: page-component-745bb68f8f-mzp66 Total loading time: 0 Render date: 2025-01-27T22:26:27.241Z Has data issue: false hasContentIssue false
  • English
  • Français

A FORMAL PROOF OF THE KEPLER CONJECTURE

Part of: Discrete geometry

Published online by Cambridge University Press:  29 May 2017

THOMAS HALES ,
MARK ADAMS ,
GERTRUD BAUER ,
TAT DAT DANG ,
JOHN HARRISON ,
LE TRUONG HOANG ,
CEZARY KALISZYK ,
VICTOR MAGRON ,
SEAN MCLAUGHLIN  and
TAT THANG NGUYEN
...Show all authors
THOMAS HALES
Affiliation:
University of Pittsburgh, USA; [email protected], [email protected]
MARK ADAMS
Affiliation:
Proof Technologies Ltd, UK Radboud University, Nijmegen, The Netherlands; [email protected]
GERTRUD BAUER
Affiliation:
ESG – Elektroniksystem- und Logistik-GmbH, Germany; [email protected]
TAT DAT DANG
Affiliation:
CanberraWeb, 5/47-49 Vicars St, Mitchell ACT 2911, Australia; [email protected]
JOHN HARRISON
Affiliation:
Intel Corporation, USA; [email protected]
LE TRUONG HOANG
Affiliation:
Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; [email protected], [email protected], [email protected], [email protected]
CEZARY KALISZYK
Affiliation:
University of Innsbruck, Austria; [email protected]
VICTOR MAGRON
Affiliation:
CNRS VERIMAG, France; [email protected]
SEAN MCLAUGHLIN
Affiliation:
Amazon, USA; [email protected]
TAT THANG NGUYEN
Affiliation:
Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; [email protected], [email protected], [email protected], [email protected]
QUANG TRUONG NGUYEN
Affiliation:
University of Pittsburgh, USA; [email protected], [email protected]
TOBIAS NIPKOW
Affiliation:
Technische Universität München, Germany; [email protected]
STEVEN OBUA
Affiliation:
University of Edinburgh, UK; [email protected]
JOSEPH PLESO
Affiliation:
Philips Electronics North America Corporation – Andover, MA, USA; [email protected]
JASON RUTE
Affiliation:
The Pennsylvania State University, USA; [email protected]
ALEXEY SOLOVYEV
Affiliation:
University of Utah, USA; [email protected]
THI HOAI AN TA
Affiliation:
Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; [email protected], [email protected], [email protected], [email protected]
NAM TRUNG TRAN
Affiliation:
Institute of Mathematics, Vietnam Academy of Science and Technology, Vietnam; [email protected], [email protected], [email protected], [email protected]
THI DIEP TRIEU
Affiliation:
AXA China Region Insurance Company Limited, Hong Kong; [email protected]
JOSEF URBAN
Affiliation:
Czech Institute of Informatics, Robotics and Cybernetics (CIIRC), Czech Republic; [email protected]
KY VU
Affiliation:
Chinese University of Hong Kong, Hong Kong; [email protected]
ROLAND ZUMKELLER
Affiliation:
[email protected]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

MSC classification

Primary: 52C17: Packing and covering in $n$ dimensions
Type
Research Article
Information
Forum of Mathematics, Pi , Volume 5 , 2017 , e2
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s) 2017

References

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
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.Google Scholar
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.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
Flyspeck, The Flyspeck Project, 2014. https://github.com/flyspeck/flyspeck.Google Scholar
GLPK, GLPK (GNU Linear Programming Kit). http://www.gnu.org/software/glpk/.Google 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
Harrison, J., The HOL Light theorem prover, 2014. http://www.cl.cam.ac.uk/∼jrh13/hol-light/index.html.Google 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
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.CrossRefGoogle Scholar
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.Google 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
Leroy, X., ‘Formal certification of a compiler back-end, or: programming a compiler with a proof assistant’, inACM SIGPLAN Notices 41, (2006), 42–54. http://compcert.inria.fr/.Google Scholar
Magron, V., ‘Formal proofs for global optimization – templates and sums of squares’. PhD Thesis, École Polytechnique, 2013.Google Scholar
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.CrossRefGoogle 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., Paulson, L. and Wenzel, M., Isabelle/HOL – A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, 2283 (Springer, 2002), http://www.in.tum.de/∼nipkow/LNCS2283/.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., ‘Formal methods and computations’. PhD Thesis, University of Pittsburgh, 2012. http://d-scholarship.pitt.edu/16721/.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
Tange, O., ‘GNU parallel – the command-line power tool’, USENIX Mag. 36(1) (2011), 42–47. URL http://www.gnu.org/s/parallel.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