Author: Roland Zumkeller
Title: Verifying inequalities over real numbers in Coq
Abstract: 
In 1611 Johannes Kepler stated that the maximal density of a
packing of spheres having the same radius is pi/sqrt(18). This value
is in fact achieved by arranging the spheres in a rather intuitive
way, as usually done by fruit sellers. Proving this conjecture
remained a challenge for several centuries - some "proofs" were given,
but they turned out to be erroneous. In 1998 Thomas C. Hales published
a proof, which is not only very large, but makes also extensive use of
computer programs (similarly to the proof of the four colour
theorem). The complexity of these calculations leaves some uncertainty
about their correctness, which has lead Hales himself to call for a
formalization of his proof. My talk will focus on one type of problem
which reoccurs throughout the proof: the formal verification of
inequalities in real numbers. A global optimization method used in
conjunction with a branch-and-bound algorithm is presented together
with its correctness proofs in Coq.