$$\newcommand{\mtn}{\mathbb{N}}\newcommand{\mtns}{\mathbb{N}^*}\newcommand{\mtz}{\mathbb{Z}}\newcommand{\mtr}{\mathbb{R}}\newcommand{\mtk}{\mathbb{K}}\newcommand{\mtq}{\mathbb{Q}}\newcommand{\mtc}{\mathbb{C}}\newcommand{\mch}{\mathcal{H}}\newcommand{\mcp}{\mathcal{P}}\newcommand{\mcb}{\mathcal{B}}\newcommand{\mcl}{\mathcal{L}} \newcommand{\mcm}{\mathcal{M}}\newcommand{\mcc}{\mathcal{C}} \newcommand{\mcmn}{\mathcal{M}}\newcommand{\mcmnr}{\mathcal{M}_n(\mtr)} \newcommand{\mcmnk}{\mathcal{M}_n(\mtk)}\newcommand{\mcsn}{\mathcal{S}_n} \newcommand{\mcs}{\mathcal{S}}\newcommand{\mcd}{\mathcal{D}} \newcommand{\mcsns}{\mathcal{S}_n^{++}}\newcommand{\glnk}{GL_n(\mtk)} \newcommand{\mnr}{\mathcal{M}_n(\mtr)}\DeclareMathOperator{\ch}{ch} \DeclareMathOperator{\sh}{sh}\DeclareMathOperator{\th}{th} \DeclareMathOperator{\vect}{vect}\DeclareMathOperator{\card}{card} \DeclareMathOperator{\comat}{comat}\DeclareMathOperator{\imv}{Im} \DeclareMathOperator{\rang}{rg}\DeclareMathOperator{\Fr}{Fr} \DeclareMathOperator{\diam}{diam}\DeclareMathOperator{\supp}{supp} \newcommand{\veps}{\varepsilon}\newcommand{\mcu}{\mathcal{U}} \newcommand{\mcun}{\mcu_n}\newcommand{\dis}{\displaystyle} \newcommand{\croouv}{[\![}\newcommand{\crofer}{]\!]} \newcommand{\rab}{\mathcal{R}(a,b)}\newcommand{\pss}[2]{\langle #1,#2\rangle} $$
Bibm@th

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 pi/racine(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. Pour mener à bien ce projet, il a lancé un appel à la communauté des mathématiciens et des informaticiens. Si vous voulez rejoindre le projet, il décrit les détails sur sa page web : http://www.math.pitt.edu/~thales/flyspeck/index.html.