Formal verification of upper bounds on translative packing densities

Abstract

Packing problems are concerned with filling the space with copies of a certain object, so that the least amount of space stays unoccupied. The famous Kepler conjecture asserts that the cannonball packing of spheres is the most efficient packing achievable, and was recently formally proven by Hales.

Dostert, Guzman, Oliveira Filho and Vallentin investigated the packing problem for other shapes. They focused on translative packings, in which all objects are oriented in the same direction. They proved several new upper bounds on translative packing densities of various Platonic and Archimedean solids. However, their results rely heavily on complex computer calculations to ensure they satisfy the conditions of a theorem.

In this thesis, proof assistant Coq is used to formally verify these conditions. An introduction to Coq is provided, aimed at the working mathematician. Then, the theorems required for the proof are developed. Several results from multivariate calculus and convexity were required for the proof, but not available in Coq. The proof also requires a large amount of floating point calculations. A method is developed to efficiently perform floating point calculations on a large scale in Coq.

Using the developed techniques, the improved upper bound of Dostert et al. on the translative packing density of the truncated tetrahedron is formally verified. These techniques can be reused to formally verify the other improved upper bounds of Dostert et al.