eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-01-17
1
11
10.4230/DagSemProc.05021.16
article
Introduction to the Flyspeck Project
Hales, Thomas C.
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.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol05021/DagSemProc.05021.16/DagSemProc.05021.16.pdf
Certified proofs
Kepler conjecture