Geodesic
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. 
@article{10_1017_fmp_2017_1,
     author = {THOMAS HALES and MARK ADAMS and GERTRUD BAUER and TAT DAT DANG and JOHN HARRISON and LE TRUONG HOANG and CEZARY KALISZYK and VICTOR MAGRON and SEAN MCLAUGHLIN and TAT~THANG NGUYEN and QUANG TRUONG NGUYEN and TOBIAS NIPKOW and STEVEN OBUA and JOSEPH PLESO and JASON RUTE and ALEXEY SOLOVYEV and THI HOAI AN TA and NAM TRUNG TRAN and THI DIEP TRIEU and JOSEF URBAN and KY VU and ROLAND ZUMKELLER},
     title = {A {FORMAL} {PROOF} {OF} {THE} {KEPLER} {CONJECTURE}},
     journal = {Forum of Mathematics, Pi},
     publisher = {mathdoc},
     volume = {5},
     year = {2017},
     doi = {10.1017/fmp.2017.1},
     language = {en},
     url = {http://geodesic.mathdoc.fr/articles/10.1017/fmp.2017.1/}
}
TY  - JOUR
AU  - THOMAS HALES
AU  - MARK ADAMS
AU  - GERTRUD BAUER
AU  - TAT DAT DANG
AU  - JOHN HARRISON
AU  - LE TRUONG HOANG
AU  - CEZARY KALISZYK
AU  - VICTOR MAGRON
AU  - SEAN MCLAUGHLIN
AU  - TAT THANG NGUYEN
AU  - QUANG TRUONG NGUYEN
AU  - TOBIAS NIPKOW
AU  - STEVEN OBUA
AU  - JOSEPH PLESO
AU  - JASON RUTE
AU  - ALEXEY SOLOVYEV
AU  - THI HOAI AN TA
AU  - NAM TRUNG TRAN
AU  - THI DIEP TRIEU
AU  - JOSEF URBAN
AU  - KY VU
AU  - ROLAND ZUMKELLER
TI  - A FORMAL PROOF OF THE KEPLER CONJECTURE
JO  - Forum of Mathematics, Pi
PY  - 2017
VL  - 5
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/articles/10.1017/fmp.2017.1/
DO  - 10.1017/fmp.2017.1
LA  - en
ID  - 10_1017_fmp_2017_1
ER  - 
%0 Journal Article
%A THOMAS HALES
%A MARK ADAMS
%A GERTRUD BAUER
%A TAT DAT DANG
%A JOHN HARRISON
%A LE TRUONG HOANG
%A CEZARY KALISZYK
%A VICTOR MAGRON
%A SEAN MCLAUGHLIN
%A TAT THANG NGUYEN
%A QUANG TRUONG NGUYEN
%A TOBIAS NIPKOW
%A STEVEN OBUA
%A JOSEPH PLESO
%A JASON RUTE
%A ALEXEY SOLOVYEV
%A THI HOAI AN TA
%A NAM TRUNG TRAN
%A THI DIEP TRIEU
%A JOSEF URBAN
%A KY VU
%A ROLAND ZUMKELLER
%T A FORMAL PROOF OF THE KEPLER CONJECTURE
%J Forum of Mathematics, Pi
%D 2017
%V 5
%I mathdoc
%U http://geodesic.mathdoc.fr/articles/10.1017/fmp.2017.1/
%R 10.1017/fmp.2017.1
%G en
%F 10_1017_fmp_2017_1
THOMAS HALES; MARK ADAMS; GERTRUD BAUER; TAT DAT DANG; JOHN HARRISON; LE TRUONG HOANG; CEZARY KALISZYK; VICTOR MAGRON; SEAN MCLAUGHLIN; TAT THANG NGUYEN; QUANG TRUONG NGUYEN; TOBIAS NIPKOW; STEVEN OBUA; JOSEPH PLESO; JASON RUTE; ALEXEY SOLOVYEV; THI HOAI AN TA; NAM TRUNG TRAN; THI DIEP TRIEU; JOSEF URBAN; KY VU; ROLAND ZUMKELLER. A FORMAL PROOF OF THE KEPLER CONJECTURE. Forum of Mathematics, Pi, Tome 5 (2017). doi: 10.1017/fmp.2017.1

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

[2] Adams, M., ‘Flyspecking Flyspeck’, inMathematical Software–ICMS 2014 (Springer, 2014), 16–20.Google Scholar | DOI

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

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

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

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

[7] Flyspeck, The Flyspeck Project, 2014. https://github.com/flyspeck/flyspeck.Google Scholar

[8] Glpk, GLPK (GNU Linear Programming Kit). http://www.gnu.org/software/glpk/.Google Scholar

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

[10] Gordon, M., Milner, R. and Wadsworth, C., Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, 78 (1979).Google Scholar | DOI

[11] 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

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

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

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

[15] 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

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

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

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

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

[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.) Lecture Notes in Computer Science, 4130 (Springer, 2006), 177–191. ISBN 3-540-37187-7.Google Scholar | DOI

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

[22] Harrison, J., ‘HOL Light: An overview’, inTheorem Proving in Higher Order Logics (Springer, 2009), 60–66.Google Scholar | DOI

[23] Harrison, J., The HOL Light theorem prover, 2014. http://www.cl.cam.ac.uk/∼jrh13/hol-light/index.html.Google Scholar

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

[25] Kaliszyk, C. and Urban, J., ‘Learning-assisted automated reasoning with Flyspeck’, J. Automat. Reason. 53(2) (2014), 173–213. .Google Scholar | DOI

[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:. URL http://www.sciencedirect.com/science/article/pii/S074771711400100X.Google Scholar | DOI

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

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

[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.) Lecture Notes in Computer Science, 8558 (Springer, 2014), 308–324. ISBN 978-3-319-08969-0..Google Scholar | DOI

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

[31] 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

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

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

[34] 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

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

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

[37] 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

[38] 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

[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.) Lecture Notes in Computer Science, 3603 (Springer, 2005), 227–244.Google Scholar | DOI

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

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

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

[43] Solovyev, A., ‘Formal methods and computations’. PhD Thesis, University of Pittsburgh, 2012. http://d-scholarship.pitt.edu/16721/.Google Scholar

[44] 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

[45] 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

[46] 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

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

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

Cité par Sources :