En 1610, Kepler décrit l'empilement de sphères dans $B R^3$ que l'on appelle aujourd'hui cubique à faces centrées, et affirme qu'il est le plus dense possible. Cette assertion, bien qu'intuitive, s'est révélée redoutablement difficile à démontrer. T. Hales et J. Ferguson y parviennent en la ramenant à un problème d'optimisation non linéaire en dimension finie ; l'ordinateur intervient de manière essentielle dans le choix du problème d'optimisation et dans sa résolution. Par une méthode similaire, T. Hales et S. McLaughlin démontrent la conjecture du dodécaèdre : le volume minimal d'une cellule de Voronoi d'un empilement de sphères identiques dans ${\bf R}^3$ est celui d'un dodécaèdre régulier circonscrit à l'une des sphères.