Introduction to the Flyspeck Project
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.
Certified proofs
Kepler conjecture
1-11
Regular Paper
Thomas C.
Hales
Thomas C. Hales
10.4230/DagSemProc.05021.16
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode