Tweet
Une preuve mathématique est vraie sans conteste, c'est une manifestation de logique pure...... Mais, selon des experts dans le domaine, un nombre croissant de démonstrations mathématiques sont désormais impossibles à vérifier avec une certitude absolue.
"Il est indéniable qu'à notre époque certains grands énoncés de mathématiques sont devenus si complexes que nous ne pouvons plus déterminer avec certitude s'ils sont vrais ou faux", fait remarquer Keith Devlin de l'Universite de Stanford en Californie.
"Cela nous met dans le même bateau que tous les autres scientifiques".
Delvin cite en exemple la Classification des groupes simples finis, une demonstration annoncée en 1980 résultant d'un travail collaboratif dans lequel de nombreux mathématiciens ont apporté chacun leur contribution. "Vingt-cinq ans plus tard nous ne sommes toujours pas sûrs qu'elle soit correcte. Nous pensons qu'elle l'est, mais personne n'a jamais rédigé la démonstration complète", indique-t-il.
"Une partie de la difficulté provient de l'usage intensif qui est fait de nos jours de l'informatique pour construire des preuves", ajoute Thomas Hales, de l'université de Pittsburgh en Pennsylvanie, "car cela rend les démonstrations moins accessibles, même aux experts".
Comment empiler des oranges ?
En 1998 Hales a proposé une démonstration assistée par ordinateur de la conjecture de Kepler, un theoreme remontant à 1611. Elle décrit la façon la plus efficace d'entasser des sphères dans une boite, en perdant le moins d'espace possible. Il apparaît que le meilleur agencement ressemble aux étalages d'oranges d'une épicerie ordinaire.
La démonstration de Hales fait plus de 300 pages de long et nécessite 40.000 lignes de code machine. Quand il a voulu la publier dans un journal scientifique, douze vérificateurs ont été affectés pour la contrôler. "Un an plus tard, ces personnes m'ont affirmé qu'ils étaient sûrs à 99% que la démonstration était correcte", indique Hales. Mais ils ont demandé à poursuivre leur évaluation.
Cette incertitude minime n'a cependant pas disparu avec le temps. Quatre ans plus tard, les inspecteurs sont revenus vers Hales, leur certitude était toujours de 99% mais cette fois ils lui ont indiqué qu'ils avaient épuisé leurs possibilités de controle. En conséquence, la revue a pris la mesure exceptionnelle de publier l'article sans une certification totale des correcteurs.
Contrôle automatisé
Même la vérification des démonstrations est désormais sous contrôle de l'informatique, selon Devlin: "pour certaines parties de la vérification, nous nous en remettons aux ordinateurs". Cette façon de procéder a connu une certaine réussite, comme pour le théorème des quatre couleurs. Cette complexite accrue n'est pas forcément complètement mauvaise. Selon Hales, il est logique d'utiliser un ordinateur pour résoudre un problème impossible à dénouer autrement.
Devlin et Hales participaient au meeting 2006 de l'AAAS (American Association for the Advancement of Science) de St Louis dans le Missouri.
Source: News Scientist
"Il est indéniable qu'à notre époque certains grands énoncés de mathématiques sont devenus si complexes que nous ne pouvons plus déterminer avec certitude s'ils sont vrais ou faux", fait remarquer Keith Devlin de l'Universite de Stanford en Californie.
"Cela nous met dans le même bateau que tous les autres scientifiques".
Delvin cite en exemple la Classification des groupes simples finis, une demonstration annoncée en 1980 résultant d'un travail collaboratif dans lequel de nombreux mathématiciens ont apporté chacun leur contribution. "Vingt-cinq ans plus tard nous ne sommes toujours pas sûrs qu'elle soit correcte. Nous pensons qu'elle l'est, mais personne n'a jamais rédigé la démonstration complète", indique-t-il.
"Une partie de la difficulté provient de l'usage intensif qui est fait de nos jours de l'informatique pour construire des preuves", ajoute Thomas Hales, de l'université de Pittsburgh en Pennsylvanie, "car cela rend les démonstrations moins accessibles, même aux experts".
Comment empiler des oranges ?
En 1998 Hales a proposé une démonstration assistée par ordinateur de la conjecture de Kepler, un theoreme remontant à 1611. Elle décrit la façon la plus efficace d'entasser des sphères dans une boite, en perdant le moins d'espace possible. Il apparaît que le meilleur agencement ressemble aux étalages d'oranges d'une épicerie ordinaire.
La démonstration de Hales fait plus de 300 pages de long et nécessite 40.000 lignes de code machine. Quand il a voulu la publier dans un journal scientifique, douze vérificateurs ont été affectés pour la contrôler. "Un an plus tard, ces personnes m'ont affirmé qu'ils étaient sûrs à 99% que la démonstration était correcte", indique Hales. Mais ils ont demandé à poursuivre leur évaluation.
Cette incertitude minime n'a cependant pas disparu avec le temps. Quatre ans plus tard, les inspecteurs sont revenus vers Hales, leur certitude était toujours de 99% mais cette fois ils lui ont indiqué qu'ils avaient épuisé leurs possibilités de controle. En conséquence, la revue a pris la mesure exceptionnelle de publier l'article sans une certification totale des correcteurs.
Contrôle automatisé
Même la vérification des démonstrations est désormais sous contrôle de l'informatique, selon Devlin: "pour certaines parties de la vérification, nous nous en remettons aux ordinateurs". Cette façon de procéder a connu une certaine réussite, comme pour le théorème des quatre couleurs. Cette complexite accrue n'est pas forcément complètement mauvaise. Selon Hales, il est logique d'utiliser un ordinateur pour résoudre un problème impossible à dénouer autrement.
Devlin et Hales participaient au meeting 2006 de l'AAAS (American Association for the Advancement of Science) de St Louis dans le Missouri.
Source: News Scientist