Abstract
We present another step, Flyspeck II, towards a complete, formal and mechanized proof of the Kepler Conjecture.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. In: Mohamed, A., Munoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 39–54. Springer, New York (2008)
Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES. Lecture Notes in Computer Science, vol. 3085, pp. 34–50. Springer, New York (2003)
Barras, B.: Programming and computing in HOL. In: Aagaard, M., Harrison, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 1869, pp. 17–37. Springer, New York (2000)
Berghofer, S.: Proofs, programs and executable specifications in higher order logic. Ph.D. thesis, Technische Universität München (2003)
Birkhoff, G.: Lattice Theory. AMS, Providence (1967)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic, New York (1979)
The COQ development team: The COQ reference manual, version 8.2. http://coq.inria.fr (2009)
Gonthier, G.: A computer-checked proof of the four color theorem. http://research.microsoft.com/~gonthier/4colproof.pdf
Gonthier, G.: Formal proof—the four color theorem. Not. Am. Math. Soc. 55 (2008)
Gordon, M.: From LCF to HOL: a short history. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 169–185. MIT, Cambridge (2000)
Gustavson, F.G.: Two fast algorithms for sparse matrices: multiplication and permuted transposition. ACM Trans. Math. Softw. 4(3), 250–269 (1978)
Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universität München (2009)
Hales, T.C.: Sphere packings III. arXiv:math/9811075v2
Hales, T.C., Ferguson, S.P.: A proof of the Kepler conjecture. Ann. Math. 162, 1065–1185 (2005)
Hales, T.C., Ferguson, S.P.: The Kepler conjecture. Discrete Comput. Geom. 36, (2006)
Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler Conjecture. Discrete Comput. Geom. (2009)
Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. Lecture Notes in Computer Science, vol. 3603. Springer, Oxford (2005)
Hölzl, J.: Proving inequalities over reals with computation in Isabelle/HOL. In: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009) (2009)
Hurd, J., Melham, T.F. (eds.): Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22–25 August 2005, Proceedings. Lecture Notes in Computer Science, vol. 3603. Springer, New York (2005)
Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR. Lecture Notes in Computer Science, vol. 4130, pp. 589–603. Springer, New York (2006)
Lang, S.: Algebra. Addison-Wesley, Reading (1974)
Nipkow, T., Bauer, G., Schultz, P.: The archive of tame graphs. http://www4.informatik.tu-muenchen.de/~nipkow/pubs/Flyspeck (2006)
Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: tame graphs. In: IJCAR, pp. 21–35 (2006)
Nipkow, T., Paulson, L.C.: Proof pearl: defining functions over finite sets. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22–25 August 2005, Proceedings. Lecture Notes in Computer Science, vol. 3603, pp. 385–396. Springer, New York (2005)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—a proof assistant for higher-order logic. In: Lecture Notes in Computer Science, vol. 2283. Springer, New York (2002)
Obua, S.: Flyspeck II: the basic linear programs. http://www4.in.tum.de/~obua/flyspeckII (2007)
Obua, S.: Proving bounds for real linear programs in Isabelle/Hol. In: Hurd, J., Melham, T.F. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, 22–25 August 2005, Proceedings. Lecture Notes in Computer Science, vol. 3603, pp. 227–244. Springer, New York (2005)
Obua, S.: Proof pearl: looping around the orbit. In: Schneider, K., Brandt, J. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 4732, pp. 223–231. Springer, New York (2007)
Obua, S.: Flyspeck II: the basic linear programs. Ph.D. thesis, Technische Universität München (2008)
Puitg, F., Dufourd, J.-F.: Formal specification and theorem proving breakthroughs in geometric modeling. In: Grundy, J., Newey, M.C. (eds.) TPHOLs. Lecture Notes in Computer Science, vol. 1479, pp. 401–422. Springer, New York (1998)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Obua, S., Nipkow, T. Flyspeck II: the basic linear programs. Ann Math Artif Intell 56, 245–272 (2009). https://doi.org/10.1007/s10472-009-9168-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-009-9168-z
Keywords
- Flyspeck
- Kepler conjecture
- Interactive theorem proving
- Isabelle
- Higher-order logic
- Computational logic
- Finite matrices
- Lattice-ordered rings
- Linear programming
- Hypermaps
- Planar graphs