Introduction to the Flyspeck Project

Author Thomas C. Hales



PDF
Thumbnail PDF

File

DagSemProc.05021.16.pdf
  • Filesize: 200 kB
  • 11 pages

Document Identifiers

Author Details

Thomas C. Hales

Cite As Get BibTex

Thomas C. Hales. Introduction to the Flyspeck Project. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006) https://doi.org/10.4230/DagSemProc.05021.16

Abstract

This article gives an introduction to a long-term project  called Flyspeck, whose purpose is to give a formal verification of the Kepler Conjecture. The Kepler Conjecture asserts that the density of a 
packing of equal radius balls in three dimensions cannot exceed $pi/sqrt{18}$. 
The original proof of the Kepler Conjecture, from 1998, relies extensively on computer calculations. Because the proof relies on relatively few external results, it is a natural choice for a formalization effort.

Subject Classification

Keywords
  • Certified proofs
  • Kepler conjecture

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail