Je ne comprends pas bien votre objection: qu’un ordinateur soit capable de vérifier les preuves des quatre médaillés de cette année ne veut pas dire qu’un programme informatique soit capable de produire ces preuves non?

Un prof nous a dit une fois (cela remonte à loin et en plus je n’étais pas très bon donc si c’est une ânerie n’hésitez pas à corriger): «Théoriquement, un ordinateur est capable d’énumérer tous les théorèmes de la théorie des groupes. Mais si on avait fait tourner cet ordinateur depuis 2000 ans, il n’en serait qu’à 1x1=1».

Ce qu’il faut éviter c’est que les journaux ne publient la preuve P’ qui, j’imagine, serait absolument incompréhensible pour un humain.

Merci pour votre message. Quelques remarques pour éclairer des points que j’aurais du expliquer.

D’abord, trouver une preuve d’un théorème est bien plus difficile et bien plus long que vérifier une preuve qu’on vous propose.

Ce que je voulais dire en parlant des articles des médaillés Fields, c’est qu’ils ne sont bien sûr pas rédigés dans une langue qu’un ordinateur pourrait lire et vérifier. Ils contiennent des phrases en français (ou en anglais suivant les cas) qui mettent en jeu des choses implicites, qui sont en principe comprises par des mathématiciens «humains» et pas par des ordinateurs !

Votre prof avait raison : on peut demander à un ordinateur d’écrire une à une toutes les preuves possibles, par ordre alphabétique en quelque sorte. Mais bien sûr, l’immense majorité des théorèmes que votre ordinateur va écrire n’auront aucun intérêt, et vous n’avez aucune idée à priori du temps que ça prendra pour voir apparaître la preuve de l’hypothèse de Riemann, si elle arrive un jour !

Je suis tout à fait d’accord avec votre dernier commentaire : il nous faut des preuves lisibles par des êtres humains... C’est un peu ce que je voulais dire en signalant qu’une preuve n’est pas seulement une suite de symboles, mais doit contenir des idées..

Etienne Ghys

Résultat fort intéressant (théoriquement), mais comme vous le dites, je doute qu’il puisse exister un jour un algorithme qui vérifie des preuves «sérieuses». Une petite question : la construction de P’ est t-elle déterministe ?

Ca rend le théorème autant plus intéressant. Avez vous des références ou liens sur ce genre de programmation, ça doit être intéressant à décortiquer.

Hop, un lien vers les preuves en informatique

Attention, cela n’est pas de même nature que le théorème PCP qui relève de la théorie de la complexité. De plus dans ce dernier, seules les preuves de taille polynomiale peuvent être encodées pour être vérifiée de manière probabiliste.

Amitiés.

Ah désolé pour le lien difficile. C’était pour répondre à Benoît ci dessus, qui dit 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.

J’ai juste voulu donner un point d’entrée sur ce projet. Je pense qu’en suivant les pages personnelles des chercheurs impliqués, on finit par trouver des éléments plus faciles.

Amicalement,

Daniel

Merci beaucoup pour les liens. En particulier DanielAugot, c’est pile ce que je cherchait.

Une info pour les lecteurs parisiens : Irit Dinur sera à Paris du 17 au 21 janvier 2011, pour un colloque mêlant informaticiens théoriciens et mathématiciens. Elle donnera un mini-cours de 3 séances, qui devrait exiger peu de connaissances préalables, voir
http://www.math.ens.fr/metric2011/