Formal verification of upper bounds on translative packing densities

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.<br/><br/>Dostert, Guzman, Oliveira Filho and...