Conjecture de Kepler: le problème est finalement résolu après 400 ans

En 1611, le physicien, mathématicien et astronome allemand Johannes Kepler a proposé que le meilleur moyen d'empiler des objets sphériques, tels que des fruits, serait de les disposer sous la forme d'une pyramide. Cependant, il ne pouvait pas prouver qu'il avait raison et ce problème énigmatique a finalement été connu sous le nom de "Conjecture de Kepler".

Selon le New Scientist, le mathématicien américain Thomas Hales a annoncé en 1998 qu’il avait été en mesure de prouver que la proposition de Kepler était correcte. À l’époque, Hales s’appuyait sur une méthode mathématique pour calculer toutes les possibilités possibles d’un théorème pour arriver à la solution.

Comptes et plus de comptes

Sur la base de cette méthode, Hales considérait que s'il existait une infinité de façons d'empiler des objets sphériques à l'infini, la plupart d'entre eux n'étaient en réalité que des variations de quelques milliers de possibilités. Ainsi, le mathématicien a divisé le problème en mille façons d'organiser des objets sphériques représentant mathématiquement les possibilités infinies d'arrangements, et a jeté toutes ces informations dans un logiciel pour effectuer les calculs.

Le résultat fut une petite pile de 300 pages qu'il a fallu quatre ans pour vérifier complètement par 12 relecteurs! Et même après tant de travail, les mathématiciens n'étaient pas totalement sûrs que les calculs étaient exacts, affirmant qu'ils n'étaient que 99% sûrs que la solution de Hales soutenait réellement la proposition de Kepler.

Enfin, 100% sûr

Eh bien, vous savez que "99% de certitude" n'est pas suffisant pour les mathématiques, non? En 2003, Hales a commencé un projet visant à prouver ses calculs, utilisant deux logiciels de vérification formels - nommés Isabelle et HOL Light - pour analyser son travail.

Et ce n'est pas qu'ils sont finalement arrivés à une conclusion! L’équipe de Hales a annoncé dimanche dernier, 10 août, qu’après avoir traduit en langage informatique les mathématiques denses présentes sur les 300 pages de calculs de 1998, elle avait pu établir que les calculs étaient corrects. En d'autres termes, après tant de siècles et d'années d'efforts de la part de Hales et de son équipe, la proposition de Kepler a été prouvée.

Et le fait que l'esprit de Kepler puisse enfin reposer en paix - et que Hales puisse attirer son attention sur un autre problème compliqué - n'est pas la seule bonne nouvelle de toute cette histoire. Cette technologie peut être utilisée pour vérifier l’énorme quantité de travail qui se produit chaque année, libérant les mathématiciens de cette tâche ingrate et leur permettant d’utiliser ce temps pour se concentrer sur d’autres questions et libérer la créativité pour explorer l’univers des nombres.