Un ordinateur confirme une théorie vieille de 400 ans

Orange

Retour en 1611 : Johannes Kepler a suggéré que la façon la plus efficace d'empiler des sphères serait d'opter pour la forme pyramidale. Concrètement, pensez à un amas d'oranges sur un étal. Malheureusement, il ne pouvait pas le prouver. Un ordinateur vient de résoudre le problème, sonnant le glas de siècles de débat.

Suivez Gizmodo sur les réseaux sociaux ! Sur TwitterFacebook ou Google+ !

Thomas Hales, de l’Université de Pittsburgh, en Pennsylvanie, a publié une preuve concernant ce problème en 1998. Toutefois, cela correspondait à un document de 300 pages. Il a fallu 12 examinateurs et quatre années pour simplement vérifier s’il y avait des erreurs. Et encore, les chercheurs n’étaient sûrs de leur coup qu’à 99%…

Amoureux des oranges ou frustré, en 2003, Hales a commencé à créer le projet Flyspeck, un outil de calcul capable de définitivement corroborer cette théorie.  Isabelle and HOL Ligh sont donc deux logiciels de vérification, aptes à valider toutes évidences logiques.

Ce dimanche, l’équipe en charge du projet a annoncé que l’ensemble des 300 pages avaient été soumises à l’analyse de ces deux programmes et, qu’à son grand soulagement, tout est juste. En d’autres termes, l’ordinateur vient de prouver avec succès que l’hypothèse avancée par Kepler il y a plus de 400 ans est correcte.

« Je me sens tout à coup dix ans plus jeune, a déclaré Hales au New Scientist« .

Evidemment, l’intérêt de ces logiciels va au-delà de savoir comment ranger des oranges dans un supermarché. Cela signifie que les mathématiciens pourront désormais se concentrer sur une pensée plus créative et laisser les ordinateurs faire le travail de vérification. Et puis, on en connait un qui va enfin dormir sur ses deux oreilles.

Tags :Sources :newscientist
Dernières Questions sur UberGizmo Help
  1. Perso je pense que les deux programmes ont uniquement été conçus pour valider cette théorie spécifiquement.
    Soyons sérieux… un programme qui vérifie les démonstrations mathématiques……

    1. Bin justement, ça fait plus de 20 ans que ça existe. Ca s’appelle Coq, Isabelle-HOL, PVS, etc. Sans compter les SAT solveurs et autres prouveurs/vérificateurs plus dédiés.

    1. Ben détrompe toi. C’était pas évident du tout. Il s’agit de la maille hexagonale compacte.
      Pour te faire réfléchir, sache que ce rangement n’est pas le plus compact quand il s’agit de ranger des oranges dans un espace clos (bordé de parois), par exemple dans un cube : les parois font que de nombreuses oranges ne peuvent plus être placées, et, dans ce cas, changer de type de rangement peut permettre de caser quelques oranges en plus.

  2. Disons plutôt qu’il se base sur des oranges, mais tu peux ainsi extrapoller sa théorie sur des atomes ou autres trucs « rond ».
    La force de la gravité a été définie aussi sur un modèle fruitier, parle en avec Newton. Et je pense aussi qu’à l’époque pas mal on du lui dire, mais tais toi donc avec ta pomme, on s’en fout de savoir si ta pomme va rebondir se mettre à voler ou autres lorsqu’elle tombe de l’arbre, faut vraiment avoir du temps à perdre.
    Et pour temps regarde maintenant ce qu’on fait des ces lois.

  3. Pourquoi ne pas avoir essayer de ranger les oranges (dont on connaît la quantité) dans une structure pyramidale qu’on rempli ensuite de liquide. De cette manière on est capable de mesurer le volume d’eau et de voir si les oranges occupent plus d’espace que dans un cube. Ok aura évidemment placé le même nombre d’orange dans le cube

Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée. Les champs obligatoires sont indiqués avec *

Publicité