The Flyspeck Project
In 1998 Thomas Hales gave a proof of the Kepler conjecture. It consists of some 300 pages of written mathematics relying on computer calculations (some 40.000 lines of code), which require several weeks.
Can the problem be considered solved? The very nature of this proof makes it difficult for a mathematician to convince himself of its correctness. While 300 pages might still be acceptable for such a prominent problem, it is virtually impossible to verify manually that the computational part is free of errors. Therefore Thomas Hales has started the "Flyspeck" project whose goal it is to develop a formal proof of the Kepler conjecture.
The Non-linear Inequalities in Hales' Proof
Given bounds on the length of the six edges of a (non-regular) tetrahedron, what can we conclude about its volume? ...about the angle at one particular edge? Questions of this kind reoccur throughout the whole proof.
To give an example, the volume of a tetrahedron can be calculated as a function of its edge lengths using the Cayley-Menger Determinant:
With this formula we obtain an optimization problem in six variables, that can be solved using interval arithmetic. Thomas Hales and his former student Samuel Ferguson did this using some C++ programs written especially for this purpose. My thesis (appendix A) takes a first step in verifying some of these inequalities in the Coq proof assistant.
Links
Here are the definitions of the involved geometric functions and the entire list of inequalites occurring in the proof (in Coq syntax).
There is a Flyspeck project page, a Flyspeck discussion group and a Flyspeck blog.
The entire proof is available here.