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}} |