En 1611, Johannes Kepler, un célèbre astronome, affirme que la manière la plus efficace pour empiler des sphères est de les disposer en forme pyramidale. Une théorie qui nous semble aujourd'hui plutôt logique dès qu'on regarde l'étal d'un primeur, mais que Kepler n'a jamais pu prouver. Qu'il se rassure, on vient d'avoir la confirmation qu'il avait raison. Joli coup Kepler !
En effet, Thomas Hales, un chercheur de l’Université de Pittsburgh, en Pennsylvanie, s'est penché sur ce problème pour tenter d'en prouver la véracité. Dès 1998, le chercheur a publié une étude prouvant que la forme pyramidale était la plus adaptée. Problème, son étude faisait 300 pages. Comment peut-on pondre 300 pages sur la meilleure manière de ranger les oranges ? Les 12 examinateurs en charge de la vérification de l'étude ont mis 4 ans et ne se sont prononcés en accord avec cette dernière qu'à 99%. On chipote un peu les gars non ?
Désireux de prouver au monde entier que sa théorie (et celle de Kepler) était bonne à 100%, Thomas Hale a relancé, en 2003, un nouveau projet baptisé Flyspeck. Il a cette fois-ci utilisé deux logiciels (Isabelle et HOL Ligh) pour valider ses affirmations définitivement. Les 300 pages du projet initial ont donc été soumises aux logiciels qui ont déclaré la véracité des dires à 100%. Alléluia ! Kepler avait raison. Et je pense que Hales peut enfin dormir sereinement. Messieurs les maraîchers, si vous hésitiez encore, vous devez désormais impérativement ranger vos oranges en pyramide pour un gain de place évident. Plus que la manière dont il faut ranger les oranges, cette découverte permet de prouver l'efficacité de certains logiciels pour vérifier des thèses scientifiques.
Par jeanlucasec, il y a 10 ans :
Je file acheter des oranges pour vérifier tout ça !
Répondre à ce commentaire
48
4