Une démonstration mathématique faite par un ordinateur… et trop grosse pour être vérifiée

Les mathématiques sont ainsi construites : on pose des axiomes de base qui ne sont autre que des principes que l’on dit vrais. Viennent alors les théorèmes qui sont des résultats établis à partir de ces axiomes de bases. Ces théorèmes sont démontrés : on est capable de dire pourquoi ils sont vrais par un raisonnement logique. Enfin, pour la plupart d’entre eux. Car, comme en physique, il existe encore de nombreuses conjectures faites par des mathématiciens et qui n’ont pas encore été démontrées. Paul Erdős était l’un deux.

Il a ainsi offert de nombreux prix pour divers problèmes mathématiques qui tiennent encore aujourd’hui. Et c’est un ordinateur qui a réussi à résoudre l’un de ces problèmes en produisant une démonstration d’une taille monstrueuse puisqu’elle est contenue dans un fichier de plus de 13 Go, ce qui la rend plus grosse que Wikipédia elle-même.

Paul Erdős en 1992

Paul Erdős en 1992

Le problème étudié s’intéresse à des suites infinies ne contenant que des +1 et des -1. Paul Erdős avait alors cherché à retrouver des motifs internes dans ces suites, en créant des sous-suites finies.

L’ordinateur en question n’a étudié qu’une partie du problème et a pourtant ainsi produit une démonstration si grosse que la faire vérifier par des humains est du domaine de l’impossible. Pourtant, toutes les démonstrations sont normalement vérifiées par d’autres mathématiciens avant d’être publiées et cette nouvelle apporte une grande question philosophique avec elle : certaines questions mathématiques sont-elles en-dehors de la portée humaine ?

Si certains affirment déjà qu’il faut rejeter cette démonstration, d’autres disent simplement qu’il suffirait que d’autres ordinateurs réussissent à établir le même résultat sans s’appuyer sur cette démonstration pour confirmer sa véracité. Quant à savoir qui a raison, c’est une autre question…

Via | Photo : Kmhkmh