L’énigme de Kepler, vieux de 400 ans, résolu

Comment empiler des objets sphériques de la façon le plus efficace ? Dans une pyramide a Johannes Kepler proposé en 1611 mais jusqu’ici aucun mathématicien n’a été en mesure de le confirmer.

Les gens ont toujours empilé boulets de canon, fruits et autres objets sphériques en pyramides. C’est une indication que la pyramide est le forme le plus efficace mais la preuve formelle a toujours manqué.

Les mathématiciens ont fait de grands efforts pour résoudre le mystère. Un entre eux est Thomas Hales, du département de mathématiques à l'Université de Pittsburgh, qui en 1998 a présenté une preuve. Son document de 300 pages a pendant 4 ans été minutieusement examiné par 12 collèges. Ils ont conclus que la preuve n’était que 99% correct.

Bien qu'il existe une infinité de manières d'empiler un nombre infini de sphères, la plupart ne sont que des variations de quelques milliers de thèmes fondamentales. D’arriver à un résultat pour chacun est évidemment un travail géantes. Hales a conclu qu’il faut de la puissance de calcul d’un ordinateur pour le faire. 

En 2003 il a lancé le projet Flyspeck avec le but de valoir des assertions logiques d’une nouvelle façon. Son équipe a utilisé deux assistants logiciels de preuves formelles appelées Isabelle et HOL Light. Les deux sont conçus autour d’un petit noyau de logique qui a été intensément scruté pour erreurs. Ils permettent de contrôler si n'importe quelle série de déclarations logiques sont vrais ou faux.  

Maintenant les membres d l'équipe Flyspeck annonce qu'ils finalement ont pu traduire tous les équations dans la preuve de Hale en formes informatisées et  conclut qu'ils sont vrais.

Selon Hales, cette forme de vérification rend contrôles par humains inutiles.

Autres mathématiciens sont impressionnés. Alan Bundy de l'Université d'Edimbourg qui n’a pas était impliqué dit : « L’effort a été énorme ». Il espère que le succès de l’équipe Flyspek inspirera d'autres mathématiciens d’utiliser les assistants de preuves. « Un mathématicien de renommée mondiale a utilisé une vérification de théorèmes automatisé. Ce fait est très important car il s’agit d’une méthode qui pourrait devenir la norme. »

Quant à Hales, il est prêt d’avancer. « J'ai une boîte pleine d'idées que j'ai mis à côté pour pouvoir travailler sur cette preuve formelle », dit-il. « Espérons que le prochain projet ne prend pas 20 ans » !

Source : New Scientist