{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T04:09:03Z","timestamp":1772510943642,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,3,17]],"date-time":"2009-03-17T00:00:00Z","timestamp":1237248000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Discrete Comput Geom"],"published-print":{"date-parts":[[2010,7]]},"DOI":"10.1007\/s00454-009-9148-4","type":"journal-article","created":{"date-parts":[[2009,3,16]],"date-time":"2009-03-16T15:50:25Z","timestamp":1237218625000},"page":"1-34","source":"Crossref","is-referenced-by-count":62,"title":["A Revision of the Proof of the Kepler Conjecture"],"prefix":"10.1007","volume":"44","author":[{"given":"Thomas C.","family":"Hales","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Harrison","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sean","family":"McLaughlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steven","family":"Obua","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roland","family":"Zumkeller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,17]]},"reference":[{"issue":"1","key":"9148_CR1","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1007\/BF03023914","volume":"8","author":"K. Appel","year":"1986","unstructured":"Appel, K., Haken, W.: The four color proof suffices. Math. Intell. 8(1), 10\u201320 (1986)","journal-title":"Math. Intell."},{"key":"9148_CR2","doi-asserted-by":"crossref","unstructured":"Bauer, G., Nipkow, T.: Flyspeck I: Tame graphs. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs. http:\/\/afp.sf.net\/entries\/Flyspeck-Tame.shtml , May 2006","DOI":"10.1007\/11814771_4"},{"key":"9148_CR3","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Automata Theory and Formal Languages, Second GI Conf., Kaiserslautern, 1975. Lecture Notes in Comput. Sci., vol. 33, pp. 134\u2013183. Springer, Berlin (1975)"},{"key":"9148_CR4","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-44659-1_8","volume-title":"TPHOLs\u201900: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics","author":"E. Denney","year":"2000","unstructured":"Denney, E.: A prototype proof translator from HOL to Coq. In: TPHOLs\u201900: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, London, UK, 2000, pp. 108\u2013125. Springer, Berlin (2000)"},{"key":"9148_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-65234-9","volume-title":"Lagerungen in der Ebene auf der Kugel und im Raum","author":"L. Fejes T\u00f3th","year":"1972","unstructured":"Fejes T\u00f3th, L.: Lagerungen in der Ebene auf der Kugel und im Raum, 2nd edn. Springer, Berlin (1972)","edition":"2"},{"issue":"1","key":"9148_CR6","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/s00454-005-1214-y","volume":"36","author":"S.P. Ferguson","year":"2006","unstructured":"Ferguson, S.P.: Sphere packings V. Pentahedral prisms. Discrete Comput. Geom. 36(1), 167\u2013204 (2006)","journal-title":"Discrete Comput. Geom."},{"key":"9148_CR7","first-page":"37","volume-title":"Proceedings of the International Symposium on Interval Mathematics on Interval Mathematics 1985","author":"J. Garloff","year":"1985","unstructured":"Garloff, J.: Convergent bounds for the range of multivariate polynomials. In: Proceedings of the International Symposium on Interval Mathematics on Interval Mathematics 1985, London, UK, 1985, pp. 37\u201356. Springer, Berlin (1985)"},{"issue":"11","key":"9148_CR8","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof\u2014the four-colour theorem. Not. Am. Math. Soc. 55(11), 1382\u20131393 (2008)","journal-title":"Not. Am. Math. Soc."},{"key":"9148_CR9","unstructured":"Hales, T.C.: Errata and revisions to the proof of the Kepler conjecture. http:\/\/code.google.com\/p\/flyspeck\/"},{"key":"9148_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02770863","volume":"17","author":"T.C. Hales","year":"1997","unstructured":"Hales, T.C.: Sphere packings. I. Discrete Comput. Geom. 17, 1\u201351 (1997)","journal-title":"Discrete Comput. Geom."},{"key":"9148_CR11","unstructured":"Hales, T.C.: Kepler conjecture source code (1998). http:\/\/www.math.pitt.edu\/~thales\/kepler98\/"},{"key":"9148_CR12","doi-asserted-by":"crossref","first-page":"1065","DOI":"10.4007\/annals.2005.162.1065","volume":"162","author":"T.C. Hales","year":"2005","unstructured":"Hales, T.C.: A proof of the Kepler conjecture. Ann. Math. 162, 1065\u20131185 (2005)","journal-title":"Ann. Math."},{"key":"9148_CR13","unstructured":"Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum f\u00fcr Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2006\/432"},{"issue":"1","key":"9148_CR14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1007\/s00454-005-1212-0","volume":"36","author":"T.C. Hales","year":"2006","unstructured":"Hales, T.C.: Sphere packings. III. Extremal cases. Discrete Comput. Geom. 36(1), 71\u2013110 (2006)","journal-title":"Discrete Comput. Geom."},{"issue":"1","key":"9148_CR15","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1007\/s00454-005-1213-z","volume":"36","author":"T.C. Hales","year":"2006","unstructured":"Hales, T.C.: Sphere packings. IV. Detailed bounds. Discrete Comput. Geom. 36(1), 111\u2013166 (2006)","journal-title":"Discrete Comput. Geom."},{"issue":"1","key":"9148_CR16","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/s00454-005-1215-x","volume":"36","author":"T.C. Hales","year":"2006","unstructured":"Hales, T.C.: Sphere packings. VI. Tame graphs and linear programs. Discrete Comput. Geom. 36(1), 205\u2013265 (2006)","journal-title":"Discrete Comput. Geom."},{"key":"9148_CR17","first-page":"35","volume-title":"LICS \u201907: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science","author":"T.C. Hales","year":"2007","unstructured":"Hales, T.C.: Some methods of problem solving in elementary geometry. In: LICS \u201907: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, 2007, pp.\u00a035\u201340. IEEE Comput. Soc., Los Alamitos (2007)"},{"key":"9148_CR18","unstructured":"Hales, T.C.: The Flyspeck Project (2007). http:\/\/code.google.com\/p\/flyspeck"},{"issue":"10","key":"9148_CR19","doi-asserted-by":"crossref","first-page":"882","DOI":"10.1080\/00029890.2007.11920481","volume":"114","author":"T.C. Hales","year":"2007","unstructured":"Hales, T.C.: The Jordan curve theorem, formally and informally. Am. Math. Mon. 114(10), 882\u2013894 (2007)","journal-title":"Am. Math. Mon."},{"key":"9148_CR20","unstructured":"Hales, T.C.: Flyspeck: A blueprint for the formal proof of the Kepler conjecture (2008). Source files at http:\/\/code.google.com\/p\/flyspeck\/source\/browse\/trunk\/"},{"key":"9148_CR21","unstructured":"Hales, T.C.: Lemmas in elementary geometry (2008). Source files at http:\/\/code.google.com\/p\/flyspeck\/source\/browse\/trunk\/"},{"issue":"11","key":"9148_CR22","first-page":"1370","volume":"55","author":"T.C. Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Not. Am. Math. Soc. 55(11), 1370\u20131380 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"1","key":"9148_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s00454-005-1209-8","volume":"36","author":"T.C. Hales","year":"2006","unstructured":"Hales, T.C., Ferguson, S.P.: The Kepler conjecture. Discrete Comput. Geom. 36(1), 1\u2013269 (2006)","journal-title":"Discrete Comput. Geom."},{"key":"9148_CR24","doi-asserted-by":"crossref","unstructured":"Hales, T.C., McLaughlin, S.: A proof of the Dodecahedral conjecture. J. Am. Math. Soc. (2009, to appear). math\/9811079","DOI":"10.1090\/S0894-0347-09-00647-X"},{"key":"9148_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201996)","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201996). Lecture Notes in Computer Science, vol. 1166, pp. 265\u2013269. Springer, Berlin (1996)"},{"key":"9148_CR26","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Theorem Proving in Higher Order Logics. Lecture Notes in Comput. Sci., vol. 3603, pp. 114\u2013129. Springer, Berlin (2005)"},{"key":"9148_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007","author":"J. Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732, pp. 102\u2013118. Springer, Kaiserslautern (2007)"},{"issue":"11","key":"9148_CR28","first-page":"1395","volume":"55","author":"J. Harrison","year":"2008","unstructured":"Harrison, J.: Formal proof\u2014theory and practice. Not. AMS 55(11), 1395\u20131406 (2008)","journal-title":"Not. AMS"},{"key":"9148_CR29","series-title":"Classics in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/b138375","volume-title":"The Analysis of Linear Partial Differential Operators. II","author":"L. H\u00f6rmander","year":"2005","unstructured":"H\u00f6rmander, L.: The Analysis of Linear Partial Differential Operators. II. Classics in Mathematics. Springer, Berlin (2005). Differential Operators with Constant Coefficients; reprint of the 1983 original"},{"key":"9148_CR30","unstructured":"IEEE Standards Committee 754. IEEE Standard for binary floating-point arithmetic, ANSI\/IEEE Standard 754-1985. Institute of Electrical and Electronics Engineers, New York (1985)"},{"key":"9148_CR31","unstructured":"Mahboubi, A., Pottier, L.: Elimination des quantificateurs sur les r\u00e9els en Coq. In: Journ\u00e9es Francophones des Langages Applicatifs (JFLA) (2002). Available on the Web from http:\/\/www.lix.polytechnique.fr\/~assia\/Publi\/jfla02.ps"},{"key":"9148_CR32","unstructured":"McLaughlin, S.: KeplerCode: computer resources for the Kepler and Dodecahedral Conjectures. http:\/\/code.google.com\/p\/kepler-code\/"},{"key":"9148_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/11814771_18","volume-title":"IJCAR","author":"S. McLaughlin","year":"2006","unstructured":"McLaughlin, S.: An interpretation of Isabelle\/HOL in HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 4130, pp. 192\u2013204. Springer, Berlin (2006)"},{"key":"9148_CR34","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated deduction\u2014CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. In: Automated deduction\u2014CADE-20. Lecture Notes in Comput. Sci., vol. 3632, pp. 295\u2013314. Springer, Berlin (2005)"},{"key":"9148_CR35","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)"},{"issue":"3","key":"9148_CR36","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1353445.1353446","volume":"30","author":"D. Monniaux","year":"2008","unstructured":"Monniaux, D.: The pitfalls of verifying floating-point computations. TOPLAS 30(3), 12 (2008)","journal-title":"TOPLAS"},{"key":"9148_CR37","series-title":"Lect. Notes in Comp. Sci.","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: In: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lect. Notes in Comp. Sci., vol. 2283. Springer, Berlin (2002). http:\/\/www.in.tum.de\/~nipkow\/LNCS2283\/"},{"key":"9148_CR38","series-title":"Lect. Notes in Comp. Sci.","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/11814771_4","volume-title":"Automated Reasoning (IJCAR 2006)","author":"T. Nipkow","year":"2006","unstructured":"Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame graphs. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning (IJCAR 2006). Lect. Notes in Comp. Sci., vol. 4130, pp. 21\u201335. Springer, Berlin (2006)"},{"key":"9148_CR39","unstructured":"Obua, S.: Flyspeck II: The basic linear programs. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2008)"},{"key":"9148_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/11814771_27","volume-title":"Automated Reasoning","author":"S. Obua","year":"2006","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Automated Reasoning. Lecture Notes in Computer Science, vol. 4130, pp. 298\u2013302. Springer, Berlin (2006)"},{"issue":"2","key":"9148_CR41","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"P.A. Parrilo","year":"2003","unstructured":"Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program., Ser. B 96(2), 293\u2013320 (2003). Algebraic and geometric methods in discrete optimization","journal-title":"Math. Program., Ser. B"},{"issue":"4","key":"9148_CR42","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/s11155-005-6891-y","volume":"11","author":"N. Revol","year":"2005","unstructured":"Revol, N., Rouillier, F.: Motivations for an arbitrary precision interval arithmetic and the MPFI library. Reliab. Comput. 11(4), 275\u2013290 (2005)","journal-title":"Reliab. Comput."},{"key":"9148_CR43","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/jctb.1997.1750","volume":"70","author":"N. Robertson","year":"1997","unstructured":"Robertson, N., Sanders, D., Seymour, P., Thomas, R.: The four-colour theorem. J. Comb. Theory, Ser. B 70, 2\u201344 (1997)","journal-title":"J. Comb. Theory, Ser. B"},{"key":"9148_CR44","unstructured":"Solovay, R.M., Arthan, R.D., Harrison, J.: Some new results on decidability for elementary algebra and geometry. APAL (2009, submitted)"},{"key":"9148_CR45","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)","edition":"2"},{"key":"9148_CR46","unstructured":"Weekes, S.: MLton. http:\/\/mlton.org"},{"key":"9148_CR47","unstructured":"Wiedijk, F.: Encoding the HOL Light logic in Coq. http:\/\/www.cs.ru.nl\/~freek\/notes\/holl2coq.pdf"},{"key":"9148_CR48","series-title":"Lecture Notes in Computer Science","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (eds.): The Seventeen Provers of the World. Lecture Notes in Computer Science, vol.\u00a03600. Springer, Berlin (2006). Foreword by Dana S. Scott, Lecture Notes in Artificial Intelligence"},{"key":"9148_CR49","unstructured":"Zumkeller, R.: Global optimization in type theory. PhD thesis, \u00c9cole Polytechnique Paris (2008)"}],"container-title":["Discrete & Computational Geometry"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00454-009-9148-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00454-009-9148-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00454-009-9148-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,3]],"date-time":"2021-10-03T07:52:12Z","timestamp":1633247532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00454-009-9148-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,17]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["9148"],"URL":"https:\/\/doi.org\/10.1007\/s00454-009-9148-4","relation":{},"ISSN":["0179-5376","1432-0444"],"issn-type":[{"value":"0179-5376","type":"print"},{"value":"1432-0444","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,17]]}}}