EasyChair Publications
Search
Paper Information
Paper:Thomas Hales
External Tools for the Formal Proof of the Kepler Conjecture
Title:External Tools for the Formal Proof of the Kepler Conjecture
Authors:Thomas Hales
Keyphrases:flyspeck, hol light, higher order logic, linear programming, kepler conjecture
Paper:
Abstract:The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the familiar cannonball arrangement. The proof of the Kepler conjecture was announced in 1998, but it went several years without publication because of the lingering doubts of referees about the correctness of the proof. In response to these publication hurdles, the Flyspeck project seeks to give a complete formal proof of the Kepler conjecture using the proof assistant HOL Light.

The original proof of the Kepler relies on long computer calculations, and these calculations present special formalization challenges. A major part of the Flyspeck project requires the integration of external computational tools with the proof assistant. Some of these external tools are the GNU linear programming kit, AMPL (a modeling language for mathematical programming), Mathematica calculations, nonlinear optimization, and custom code in C++, C, C#, Java, and Objective Caml.

Earlier work by A. Solovyev has implemented efficient linear programming in HOL Light. This talk will include a description of his more recent work that automates the link between linear programming and the Flyspeck project.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:1
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:19
Downloads:6
BibTeX entry:
@inproceedings{PxTP2013:External_Tools_for_the_Formal_Proof_of_the_Kepler_Conjecture,
  author    = {Thomas C. Hales},
  title     = {External Tools for the Formal Proof of the Kepler Conjecture},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {1},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}