Empilements de Képler

En 1609, l'astronome allemand Johannes Kepler s'est attaqué au problème de l'empilement de sphères le plus dense possible. Autrement dit, comment ranger des oranges dans un carton afin d'en disposer le plus possible. Kepler propose de commencer par répartir les oranges au fond du carton de sorte que chaque orange soit entourée de 6 autres formant un hexagone régulier. Il répète l'opération sur la couche supérieure, mais avec un décalage (on dispose les oranges dans les "trous" laissés par les oranges du rang précédent), et ainsi de suite... On obtient deux formes possibles, suivant que la 3ème couche est superposée à la première ou non. En cristallographie, on parle d'empilement hexagonal compact et d'empilement cubique à faces centrées. La densité de ces empilements est alors $\frac{\pi}{\sqrt{18}}.$

Selon Kepler, ces solutions sont les meilleures possibles : on ne peut pas ranger les oranges de façon plus dense! Ceci semble intuitivement vrai, d'autant que cette conjecture est confirmée par la nature, puisque c'est ainsi que se disposent les atomes de zinc, de cuivre ou d'aluminum. Mais, avant 1998, on n'avait jamais trouvé de preuve mathématique à cela. Thomas Hales en propose une en cette année 1998, et sa démonstration est aussi longue que difficile. Surtout elle fait appel à l'outil informatique de manière nouvelle et impressionante : plus de 3gigaoctets de programmes et de données sont nécessaires dans sa preuve! Une équipe de 12 chercheurs mandatée par la prestigieuse revue Annals of Mathematics se charge de vérifier la véracité de la preuve. Après plus de 4 ans de travail, elle a rendu le verdict suivant : selon elle, la preuve est valide à 99%, mais elle se déclare incompétente pour vérifier certains détails et calculs.

Ne voulant se contenter de cette opinion globalement positive, T. Hales a lancé le projet Flyspeck, qui se propose de trouver une preuve formelle de la conjecture de Képler, c'est-à-dire un ensemble de déductions dans le langage de la logique qui mène à la preuve de la conjecture. C'est chose faite en 2014, une preuve formelle est écrite grâce au logiciel “HOL Light.”