Elamur Research⌕
☰
home / papers / 2015 / A formal proof of the Kepler conjecture

A formal proof of the Kepler conjecture

Paper · 2015 · Thomas Hales, Mark Adams, Gertrud Bauer et al.

Summary

The Kepler conjecture claims that no arrangement of equal balls in three-dimensional space is denser than the face-centered cubic packing, whose density is π/√18 (about 0.74). Ferguson and Hales proved it in 1998. Their argument depended so heavily on computer calculations that referees could not fully certify it, and it appeared in 2006 without complete endorsement. This paper is the official report on Flyspeck, a project announced in 2003 to remove that doubt by machine-checking the whole argument. The team formalized both the conventional mathematical reasoning and three large computational components: nonlinear inequalities, an enumeration of tame plane graphs, and linear programs. They used the HOL Light and Isabelle proof assistants, where correctness ultimately rests on small, heavily scrutinized logical kernels. The verified statement bounds the number of packing points inside a finite spherical container, up to an error term that becomes negligible as the container grows. It ranks among the largest verification efforts by code size. It settles a centuries-old problem far more reliably than peer review can, and it inspired new tools for proof translation, automation and auditing.

Key points

  • The formalization uses HOL Light and Isabelle/HOL, with an independent re-check of the main statement in HOL Zero. Supporting tools include OCaml, CamlP5 and GLPK, and the Isabelle parts are in the Archive of Formal Proofs.
  • The central HOL Light theorem shows that the nonlinear inequalities (nearly 1,000 of them) and the tame graph classification together imply the conjecture. It runs in about 5 hours on a 2 GHz CPU, or roughly 40 minutes in recorded-proof format.
  • The tame plane graph classification was verified in Isabelle, and the 43,078 linear programs were checked in about 15 hours on a 2.4 GHz machine using integer-scaled dual solutions. The most demanding computational subclaim needs around 5,000 CPU hours.
  • The authors see their main weak spot as the manual transfer of the tame classification statement from Isabelle into HOL Light. Auditors should confirm that both systems use an identical graph list.
  • The Flyspeck codebase is comparable in scale to Feit-Thompson, CompCert and seL4. It may hold the record for lines of code in a verification project.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Imperial College LondonLondon · United Kingdom56 works · 13,671 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksMathematics · 233 worksNumerical Analysis · 6 worksAlgebra and Number Theory · 2 works

Cite

Cite as Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu and Roland Zumkeller. 2015. A formal proof of the Kepler conjecture. arXiv:1501.02155.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.1501.02155 · arXiv 1501.02155

@misc{hales2015formal,
  title = {{A formal proof of the Kepler conjecture}},
  author = {Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong {Le Hoang}, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu and Roland Zumkeller},
  year = {2015},
  doi = {10.48550/arxiv.1501.02155},
  eprint = {1501.02155},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1501.02155}
}

References

42 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Hales et al. Biha, et al. A machine-checked proof of the odd order theorem. In Interactive Theorem Proving, pages 163–179. Springer, 2013. find
  2. [10] Michael Gordon, Robin Milner, and Christopher Wadsworth. Edinburgh LCF: a mechanized logic of computation, volume 78 of lecture notes in computer science, 1979. find
  3. [11] Michael JC Gordon and Tom F Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993. find
  4. [12] Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19-21, 2010. Proceedings, pages 103–117, 2010. doi: 10.1007/978-3-642-12251-4 9. URL http://dx.doi.org/10.100… — [doi:10.1007/978-3-642-12251-4](https://doi.org/10.1007/978-3-642-12251-4) find
  5. [13] Thomas Hales. Developments in formal proofs. Bourbaki Seminar, (1086), 2014. find
  6. [14] Thomas C. Hales. Dense Sphere Packings: a blueprint for formal proofs, volume 400 of London Math Soc. Lecture Note Series. Cambridge University Press, 2012. find
  7. [15] Thomas C. Hales. A proof of the Kepler conjecture. Annals of Mathematics, 162: 1063–1183, 2005. find
  8. [16] Thomas C Hales. The strong dodecahedral conjecture and Fejes Tóth’s contact conjecture. Technical report, 2011. find
  9. [17] Thomas C. Hales. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum für Informatik… find
  10. [18] Thomas C. Hales and Samuel P. Ferguson. The Kepler conjecture. Discrete and Computational Geometry, 36(1):1–269, 2006. find
  11. [19] Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller. A revision of the proof of the Kepler Conjecture. Discrete & Computational Geometry, 44(1):1–34, 2010. find
  12. [20] John Harrison. Towards self-verification of HOL Light. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 177–191. find
  13. Springer, 2006. ISBN 3-540-37187-7. doi: 10.1007/11814771 17. URL http://dx.doi.org/10.1007/11814771_17. — [doi:10.1007/11814771](https://doi.org/10.1007/11814771) ↗
  14. [21] John Harrison. The HOL Light theorem prover, 2014. http://www.cl.cam.ac. uk/˜jrh13/hol-light/index.html. ↗
  15. [22] John Harrison. Without loss of generality. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pages 43–59, M… find
  16. [23] John Harrison. HOL Light: An overview. In Theorem Proving in Higher Order Logics, pages 60–66. Springer, 2009. find
  17. [24] Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), volume 7998 of LNCS, pages 51–66. Springer, 2013. find
  18. A formal proof of the Kepler conjecture Hales et al. [25] Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014. doi: 10.1007/s10817-014-9303-3. URL http://dx.doi.org/10.1007/s10817-014-9303-3. ↗
  19. [26] Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. Journal of Symbolic Computation, (0):–, 2014. ISSN 0747-7171. doi: http://dx.doi.org/10.1016/j.jsc.2014.09.032. URL http://www.sciencedirect. com/science/article/pii/S074771711400100X. — [doi:10.1016/j.jsc.2014.09.032](https://doi.org/10.1016/j.jsc.2014.09.032) ↗
  20. [27] Johannes Kepler. Strena seu de nive sexangula. Frankfurt: Gottfried. Tampach, 1611. [28] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood.… find
  21. [29] Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens. HOL with definitions: Semantics, soundness, and a verified implementation. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VS… find
  22. Springer, 2014. ISBN 978-3-319-08969-0. doi: 10.1007/978-3-319-08970-6 20. URL http://dx.doi.org/10.1007/978-3-319-08970-6_20. — [doi:10.1007/978-3-319-08970-6](https://doi.org/10.1007/978-3-319-08970-6) ↗
  23. [30] J. Lagarias. The Kepler Conjecture and its proof, pages 3–26. Springer, 2009. find
  24. [31] Xavier Leroy. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. 33rd ACM symposium on Principles of Programming Languages, pages 42–54, 2006. http://compcert.inria.fr/. ↗
  25. [32] Victor Magron. Formal Proofs for Global Optimization – Templates and Sums of Squares. PhD thesis, École Polytechnique, 2013. find
  26. [33] Christian Marchal. Study of the Keplers conjecture: the problem of the closest packing. Mathematische Zeitschrift, 267(3-4):737–765, 2011. ISSN 0025-5874. doi: 10.1007/s00209-009-0644-2. URL http://dx.doi.org/10.1007/s00209-009-0644-2. — [doi:10.1007/s00209-009-0644-2](https://doi.org/10.1007/s00209-009-0644-2) ↗
  27. [34] Sean McLaughlin. An interpretation of Isabelle/HOL in HOL Light. In Ulrich Furbach and Natarajan Shankar, editors, IJCAR, volume 4130 of Lecture Notes in Computer Science, pages 192–204. Springer, 2006. find
  28. [35] Ramon E Moore, R Baker Kearfott, and Michael J Cloud. Introduction to interval analysis. Siam, 2009. find
  29. [36] Tobias Nipkow. Verified efficient enumeration of plane graphs modulo isomorphism. In Van Eekelen, Geuvers, Schmaltz, and Wiedijk, editors, Interactive Theorem Proving (ITP 2011), volume 6898 of Lect. Notes in Comp. Sci., pages 281–296. find
  30. [37] Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of Lect. Notes in Comp. Sci. Springer-Verlag, 2002. http://www.in.tum.de/˜nipkow/LNCS2283/. ↗
  31. [38] Tobias Nipkow, Gertrud Bauer, and Paula Schultz. Flyspeck I: Tame graphs. In U. Furbach and N. Shankar, editors, Automated Reasoning (IJCAR 2006), volume 4130 of Lect. Notes in Comp. Sci., pages 21–35. find
  32. [39] Steven Obua. Proving bounds for real linear programs in Isabelle/HOL. In J. Hurd and T. F. Melham, editors, Theorem Proving in Higher Order Logics, volume 3603 A formal proof of the Kepler conjecture Hales et al. of Lect. Notes in Comp. Sci., pages 227–244. Springer-Verlag, 2005. find
  33. [40] Steven Obua. Flyspeck II: The Basic Linear Programs. PhD thesis, Technische Universität München, 2008. find
  34. [41] Steven Obua and Tobias Nipkow. Flyspeck II: the basic linear programs. Annals of Mathematics and Artificial Intelligence, 56(3–4), 2009. find
  35. [42] Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 298– 302. Springer, 2006. find
  36. [43] Alexey Solovyev. Formal Methods and Computations. PhD thesis, University of Pittsburgh, 2012. http://d-scholarship.pitt.edu/16721/. ↗
  37. [44] Alexey Solovyev and Thomas C. Hales. Efficient formal verification of bounds of linear programs, volume 6824 of LNCS, pages 123–132. Springer-Verlag, 2011. find
  38. [45] Alexey Solovyev and Thomas C. Hales. Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations. In NFM, volume 7871 of LNCS, pages 383– 397. 2013. find
  39. [46] O. Tange. GNU parallel - the command-line power tool. ;login: The USENIX Magazine, 36(1):42–47, Feb 2011. URL http://www.gnu.org/s/parallel. ↗
  40. [47] Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers. Formal mathematics on display: A wiki for Flyspeck. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, MKM/Calculemus/DML, volume 7961 of LNCS, pages 152–167. Springer, 2013. ISBN 9… find
  41. [48] Roland Zumkeller. Global Optimization in Type Theory. PhD thesis, École Polytechnique Paris, 2008. find
  42. A formal proof of the Kepler conjecture find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/hales-2015-formal-proof-kepler-conjecture/