DagSemProc.05021.16.pdf
- Filesize: 200 kB
- 11 pages
Document
Introduction to the Flyspeck Project
Author
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 5021
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2006-01-17
Cite AsGet 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
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.
Keywords
- Certified proofs
- Kepler conjecture
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads