Invité a écrit :Que valent les démonstrations de théorèmes mathématiques qui sont faites par ordinateurs ? Ces "preuves" informatiques qui utilisent une nombre astronomique de petits pas logiques pour arriver à leur fin.
Pas sur que notre cerveau ne fonctionne pas lui aussi ainsi, du moins partiellement.
Un sérieux problème se pose aux éditeurs de revues spécialisées comme Annals of Mathematics. Ils ne peuvent plus procéder à l'étape de l'évaluation par des pairs (peer-reviews) de ces nouvelles démonstrations qui leur sont soumises pour publication. Ces démonstrations ressemblent plus à du code de programmation qu'a un article scientifique. Ces preuves formelles pas ordinateurs sont a toute fin pratique illisibles ! Des articles de ce genre sont restés plusieurs années sur les tablettes des éditeurs de revues mathématiques faute de pouvoir les faire reviser par des pairs.
Le theoreme de classification des groupes finis pose lui aussi quelques menus problemes. Il s'agit d'un patchwork de plusieurs milliers de pages pondues par plus de cent mathematiciens et, a ma connaissance, le seul mathematicien - Gorenstein - qui en avait une vue d'ensemble la moins parcellaire est decede.
Faudra-t-il attendre la mise au point de méthodes formelles de vérification qui pourront faire la preuve de la justesse de ces démonstrations faites par ordinateurs ?
C'est le cas - au moins en partie - de la preuve du theoreme des quattre couleurs version Gonthier.
On risque de tourner en rond un tiboutte de temps, car comment fera-t-on la preuve de la bonne marche de ces outils vérificateurs de démonstrations formelles ?
La demonstration automatique n'en est qu'a ses premiers pas, mais ils sont prometteurs (voir par exemple
COQ).
Le type de "preuve" proposee par Appel et Haken (theoreme des quattre couleurs) ou par Hales (theoreme de Kepler) peut donner des boutons - c'est mon cas - parce qu'elle est confinee a une suite de calculs sur des classes de cas de figure: il s'agi(ssa)it donc d'utiliser l'ordinateur comme une "calculette". Cependant, si l'on a affaire a des preuves "enumeratives" (c'est l'idee de la preuve d'Appel et Haken et de Hales, a quelques variantes pres), l'utilisation massive de "calculettes" peut etre l'unique echappatoire, helas. Mais la preuve proposee par
Gonthier est d'un tout autre type (elle s'appuie implicitement sur le theoreme de Goedel-Herbrand, sur les isomorphismes de Curry-Howard et sur un tas d'autres trucs connexes a tout ce qui touche a la demonstration automatique - et bien sur, sur la preuve "ecourtee" de
Robertson, Sanders, Seymour et Thomas): elle permet en effet non seulement d'effectuer des calculs sur des classes de cas de figure, mais egalement de verifier les enchainements logiques en soi. Cela ressemble donc deja beaucoup plus a ce que l'on entend aujourd'hui par preuve. Bref, c'est moins irritant. En attendant une jolie preuve qui tiendrait dans une marge...
groucho max
