Invited Paper: Some Methods of Problem Solving in Elementary Geometry (at LICS 2007)

Authors: Thomas C. Hales

Abstract

Many elementary problems in geometry arise as part of the proof of the Kepler conjecture on sphere packings. In the original proof, most of these problems were solved by hand. This article investigates the methods that were used in the original proof and describes a number of other methods that might be used to automate the proofs of these problems. A companion article presents the collection of elementary problems in geometry for which automated proofs are sought. This article is a contribution to the Flyspeck project, which aims to give a complete formal proof of the Kepler conjecture.

BibTeX

  @InProceedings{Hales-SomeMethodsofProble,
    author = 	 {Thomas C. Hales},
    title = 	 {Some Methods of Problem Solving in Elementary Geometry},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {35--40},
    location =   {Wroclaw, Poland}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }