"une notion qui empoisonne les mathématiques"

Quelle logique pour les démonstrations mathématiques calculatoires ?
Gilles Dowek - Professeur à l'École Polytechnique
Jeudi 19 avril au LINA, fac des sciences de Nantes
================================================


On utilise de plus en plus souvent des calculs (et des ordinateurs) pour
démontrer des théorèmes comme
"La cinq centième décimale de pi est un 2", "le nombre 22976221-1 est
premier", "le pont P supporte
une charge m", "toute carte est coloriable avec quatre couleurs", "le
réseau cubique face centré est une
manière optimale d'empiler des oranges", ... La logique "axiomatique"
traditionnelle n'est pas adaptée pour
exprimer de telles démonstrations et il devient nécessaire de la faire
évoluer pour donner, ou re-donner,
une place au calcul dans les démonstration logiques. Cette idée est
présente, au moins implicitement, depuis
le début des années 70, dans plusieurs travaux de logique et
d'informatique, qui ne sont pas toujours reliés
les uns aux autres. Ce retour du calcul permet aussi de résoudre des
problèmes internes à la logique et
nous montre qu'il est peut-être possible de se passer d'une notion qui
empoisonne les mathématiques depuis
deux millénaires : la notion d'axiome.

Gilles Dowek a écrit des livres de "popular science" sur la Logique.