Comment l’ordinateur peut vérifier les mathématiques : L’exemple du théorème des quatre couleurs
Benjamin Werner (INRIA et Ecole Polytechnique)

Infos Complémentaires

Ces séminaires ont lieu le jeudi à 13h30 en salle de conférence IV au 2ème étage du batiment dit "de chimie".

Jeudi 7 fevrier

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
nouveau. 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 systèmes de preuves peuvent
apporter une réponse à cette situation, et ce que cela implique dans
notre rapport à la vérité mathématique.

Ces séminaires ont lieu le jeudi à 13h30 en salle de conférence IV au 2ème étage du batiment dit "de chimie".