# Introduction to the Flyspeck Project

@inproceedings{Hales2005IntroductionTT, title={Introduction to the Flyspeck Project}, author={Thomas C. Hales}, booktitle={Mathematics, Algorithms, Proofs}, year={2005} }

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.

#### Topics from this paper

#### 97 Citations

A Revision of the Proof of the Kepler Conjecture

- Mathematics, Computer Science
- Discret. Comput. Geom.
- 2010

The current status of a long-term initiative to reorganize the original proof of the Kepler conjecture into a more transparent form and to provide a greater level of certification of the correctness of the computer code and other details of the proof is summarized. Expand

A FORMAL PROOF OF THE KEPLER CONJECTURE

- Mathematics, Computer Science
- Forum of Mathematics, Pi
- 2017

This paper constitutes the official published account of the now completed Flyspeck project and describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. Expand

hosted at the Radboud Repository of the

- 2018

This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published… Expand

The HOL Light Theory of Euclidean Space

- Computer Science
- Journal of Automated Reasoning
- 2012

This formalization was started in 2005 and has been extensively developed since then, partly in direct support of the Flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic analytical, geometrical and topological machinery. Expand

Certification of Bounds of Non-linear Functions: The Templates Method

- Mathematics, Computer Science
- MKM/Calculemus/DML
- 2013

An approximation algorithm, which combines ideas of the max-plus basis method (in optimal control) and of the linear templates method developed by Manna et al. (in static analysis), is introduced, which leads to semialgebraic optimization problems, solved by sum-of-squares relaxations. Expand

Ordered geometry in Hilbert's Grundlagen der Geometrie

- Mathematics
- 2015

The Grundlagen der Geometrie brought Euclid’s ancient axioms up to the standards of modern logic, anticipating a completely mechanical verification of their theorems. There are five groups of axioms,… Expand

Formal computations and methods

- Computer Science
- 2012

This work is an integral part of the Flyspeck project (a formal proof of the Kepler conjecture) and it is shown how developed formal procedures solve formal computational problems in this project. Expand

Formal Proofs for Nonlinear Optimization

- Mathematics, Computer Science
- J. Formaliz. Reason.
- 2015

The implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates and produces both valid underestimators and lower bounds for each approximated constituent. Expand

From informal to formal proofs in Euclidean geometry

- Computer Science
- Annals of Mathematics and Artificial Intelligence
- 2018

A TPTP inspired language is used to write a semi-formal proof of a theorem, that fairly accurately depicts a proof that can be found in mathematical textbooks. Expand

Formal Proofs for Global Optimization - Templates and Sums of Squares. (Preuves formelles pour l'optimisation globale - Méthodes de gabarits et sommes de carrés)

- Mathematics, Computer Science
- 2013

The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions and to prove their correctness by checking the certificates in the Coq proof system, using a software package named NLCertify. Expand

#### References

SHOWING 1-10 OF 28 REFERENCES

Some Algorithms Arising in the Proof of the Kepler Conjecture

- Mathematics
- 2002

By any account, the 1998 proof of the Kepler conjecture is complex. The thesis underlying this article is that the proof is complex because it is highly under-automated. Throughout that proof, manual… Expand

An overview of the Kepler conjecture

- Mathematics
- 1998

This is the first in a series of papers giving a proof of the Kepler conjecture, which asserts that the density of a packing of congruent spheres in three dimensions is never greater than… Expand

Sphere packings, I

- Mathematics, Computer Science
- Discret. Comput. Geom.
- 1997

A program to prove the Kepler conjecture on sphere packings is described and it is shown that every Delaunay star that satisfies a certain regularity condition satisfies the conjecture. Expand

Bounds for Local Density of Sphere Packings and the Kepler Conjecture

- Computer Science, Mathematics
- Discret. Comput. Geom.
- 2002

The particular local density inequality underlying the Hales and Ferguson approach to prove Kepler’s conjecture is described and some features of their proof are sketched. Expand

The Jordan-Scho¨nflies theorem and the classification of surfaces

- Mathematics
- 1992

INTRODUCTION. The Jordan curve theorem says that a simple closed curve in the Euclidean plane partitions the plane into precisely two parts: the interior and the exterior of the curve. Although this… Expand

Theory on plane curves in non-metrical analysis situs

- Mathematics
- 1905

JORDAN'St explicit formulation of the fundamental theorem that a simple closed curve lying wholly in a plane decomposes the plane into an inside and an outside region is justly regarded as a most… Expand

The Kissing Problem in Three Dimensions

- Mathematics, Computer Science
- Discret. Comput. Geom.
- 2006

A new solution of the Newton--Gregory problem is presented that uses the extension of the Delsarte method and relies on basic calculus and simple spherical geometry. Expand

A Proof of the

- Mathematics
- 2006

We present a new proof of the version of the Shauder-Tychonov theorem provided by Coppel in Stability and Asymptotic Behavior of Difierential Equations, Heath Mathematical Monographs, Boston (1965).… Expand

A Proof-Producing Decision Procedure for Real Arithmetic

- Computer Science, Mathematics
- CADE
- 2005

This is the first generally useful proof-producing implementation of a quantifier elimination procedure for real closed fields, and convincing examples of its value in interactive theorem proving are demonstrated. Expand

Euclidean and Non-Euclidean Geometry: An Analytic Approach

- Mathematics
- 1986

Preface Notation and special symbols Historical introduction 1. Plane Euclidean geometry 2. Affine transformations in the Euclidean plane 3. Finite groups of isometries of E2 4. Geometry on the… Expand