2006/01/01 by Thomas Hales, Hales, Thomas C. · 2 citations
Mathematics · Physics and Astronomy · #Advanced Mathematical Theories and Applications #Certified proofs #History and Theory of Mathematics #Kepler conjecture #Mathematics and Applications
paper · doi:10.4230/dagsemproc.05021.16
openalex publication_date 2006/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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/sqrt18. 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.