Comment l'ordinateur peut vérifier les mathématiques. L'exemple du théorème des quatre couleurs.

par M. Benjamin Werner (INRIA et Ecole Polytechnique)

mardi 7 avr. 2009, 11:00 → 12:00 US/Central

Salle 101

L'ordinateur peut intervenir de plusieurs manières dans l'argumentation mathématique. D'une part, sa puissance de calcul permet d'énoncer des faits nouveaux. Par exemple que 2 à la puissance 32.582.657 moins 1 est premier. D'autre part, la précision de la machine lui permet de vérifier qu'une démonstration mathématique est correcte, c'est-à-dire qu'elle suit bien les règles de la logique. Un logiciel effectuant cette tâche est appelé un système de preuves. On arrive maintenant à combiner ces deux aspects. C'est la cas pour le théorème des quatre couleurs, dont la preuve repose partiellement, sur un calcul trop important pour être humainement faisable. On est donc obligé de faire confiance à l'ordinateur pour se convaincre de ce résultat. J'essayerai d'expliquer comment les sytèmes de preuves peuvent apporter une réponse à cette situation, et ce que cela implique dans notre rapport à la vérité mathématique. J'aborderai également quelques analogies avec la physique ainsi que des conséquences possibles pour la "physique sur ordinateur".

Minutes BWerner-coq.pdf

Poster SemB.Werner.pdf