Vérifier une preuve : la conférence de Irit Dinur
le 25 août 2010 à 10:42, par Benoît Kloeckner
Tout d’abord, n’oublions pas que les travaux d’Irit Dinur peuvent s’appliquer en informatique sur des « certificats », c’est-à-dire des preuves putatives qu’une certaine proposition est correcte. On peut vouloir certifier des énoncés mathématiques intéressants, mais aussi des calculs et des programmes.
Ensuite, vous vous trompez : on sait déjà écrire dans des langage vérifiables par ordinateur des preuves très sérieuses. Le théorème des quatre couleurs a par exemple été vérifié ainsi. J’ai entendu parler d’un projet stupéfiant : une équipe de recherche s’attaque à la vérification par ordinateur de la classification des groupes finis simple.
C’est à mon avis très intéressant, car cette classification est tellement longue à obtenir, tellement dispersée dans la littérature, qu’on n’est pas complètement sûrs que la preuve soit juste.
En fait, je préfèrerais encore qu’on trouve à ces résultats des démonstrations assez simples pour être entièrement vérifiées par un être humain en un temps raisonnable, mais un certificat informatique est tout de même loin d’être négligeable.
Il faut aussi se rappeler qu’il y a forcément des énoncés simple, vrai (et même démontrable) qui n’ont pas de démonstration courte. Évidemment, on ne sait pas lesquels !
Répondre à ce message