Le conjecture de Kepler
Les plus grandes énigmes mathématiques sont parfois nées dans le quotidien le plus basique.
Si vous allez chez un légumiste, vous noterez que le présentoir des oranges est toujours disposé de la même manière.
Il y a d’abord une première strate d’oranges et puis la seconde strate est constituée en plaçant les oranges dans les trous de la première strates et ainsi de suite.
Cette chose forme un empilement d’oranges qui se resserre au fur et à mesure des strates, en une sorte de pyramide.
La question est de savoir si cet empilement subtil est le plus efficace. En d’autres termes, réussit-on à mettre le plus d’oranges possibles dans un espace donné en les empilant comme chez le légumiste.
Alors là, j’espère que vous êtes bien assis car devinez de quand date la première formulation de cette conjecture.
Tout juste, elle avait été formulée par Kepler, Johannes, l’astronome allemand en 1611. On l’appelle conjecture d Kepler.
Il parlait pas d’oranges, les légumes c’était pas son truc, mais de sphères parfaites.
C’est ici que les Romains s’empoignèrent car la conjecture a de tout temps été supposée vraie, en tout cas rien n’indiquait aux savants qu’elle fût fausse mais on n’arrivait pas à la démontrer.
La démonstration est arrivée, tenez-vous bien, en 1998 grâce un mathématicien états-unien (Thomas Hales).
Déjà, on se dit que quatre cent ans pour démontrer ce que fait mon marraîcher tous les wouikande, il faut pas être pressé dans le monde mathématique.
Mais l’histoire n’est pas terminée.
On n’a pas fait une démonstration "un puis deux puis trois" comme on nous apprend à l’école, car la conjecture des oranges est trop complexe.
On a donc ramené le problème des oranges à un savant mélange de morceaux de démonstrations formels très alambiqués et de simulations numériques très alambiquées aussi. Bref, c’était très alambiqué.
Vu que les camarades mathématiciens n’avaient pas toute la vie devant eux, ils ont voulu signaler au monde qu’ils avaient d’après eux résolu les oranges.
Ils ont publié le résultat dans une revue ultra-prestigieuse, le top du top du bazar : "Annals of Mathematics".
C’est ici qu’il y a l’os dans le potage.
Toute publication scientifique nécessite vérification par des autres scientifiques du même domaine logiquement qu’on appelle les pairs (les égaux). Ces fameux pairs chargés de vérifier la démonstration des oranges ont passé quatre ans à cogiter et…
…Ils n’ont pas réussi ! Au bout des 4 ans, ils savaient pas dire si la preuve était juste ou fausse ! La preuve semblait juste sans pouvoir le dire tout à fait officiellement avec la certitude absolue.
On était gros Jean comme devant pour le dire platement et puis imaginez la tête des maraichers à qui on viendrait expliquer qu’on sait toujours pas exactement s’ils empilent leurs oranges correctement.
Pour résoudre le bazar, les matheux se sont dits : si les humains sont pas capable, demandons aux ordinateurs.
Les ordinateurs peuvent effectuer des démonstration ?
C’est une toute nouvelle branche des mathématiques aux confins de l’intelligence artificielle. On appelle ces programmes des assistants de preuves formelles.
Attention et minute papillon : même un ordinateur tout puissant qu’il est ne vérifie pas des conjectures aussi complexes que les oranges sur un coin de table.
La vérification a mobilisé dix ans de calculs et tout un tas de chercheurs. Faut pas être pressé (orange pressé)
En 2014, on a formellement démontré l’empilement l’empilement des oranges.
Enfin, quand je dit "on a démontré" c’est volontairement vague.
Aucun humain n’est capable de faire la démonstration de but en blanc. Personne ne comprend totalement la démonstration des oranges.
Salukes
#ConjectureDeKepler
#EmpilementOptimisé
#MathématiquesComplexes
#HistoireDesMathématiques
#SimulationNumérique
