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.
RECRUITMENT DIRECT ACCESS
The Department of Physics
Fête de la Science 2018 