Vérifier une preuve : la conférence de Irit Dinur
le 24 août 2010 à 15:18, par Étienne Ghys
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épondre à ce message