Par honnêteté, j'avertis le lecteur que je connais Gilles Dowek, que nous enseignons dans le même cours et que nous travaillons dans des domaines scientifiques connexes. Bref, il est possible que je ne sois pas objectif.

On pourrait résumer cet ouvrage de façon provocante en disant qu'il expose l'évolution de la nature des démonstrations mathématiques formelles au cours du temps en la faisant aboutir en apothéose sur les preuves calculatoires en théorie des types d'ordre supérieur, ce qui est justement le thème de travail de Gilles Dowek (thème au demeurant tout à fait intéressant).

Plus sérieusement, l'ouvrage se penche sur le rapport entre deux aspects des mathématiques : d'une part le calcul (en commençant par les calculs arithmétiques simples, puis en étendant à la notion d'algorithme), d'autre part les démonstrations. Les démonstrations, assimilées à un raisonnement donc à la pensée, ont longtemps été considérées comme la partie noble des mathématiques. Cependant, au 20ème siècle, les résultats de Turing, Church, Gödel, Rosser etc. ont établi un lien étroit entre démonstration et calcul, notamment grâce au fait que les démonstrations bien formées peuvent être énumérées par un algorithme.

Un autre lien a été établi par la théorie des types : une démonstration est un algorithme qui produit les conclusions à partir des hypothèses. On parle de correspondance de Curry-Howard, bien que ce terme n'apparaisse pas dans l'ouvrage de Gilles Dowek.

L'ouvrage évoque avec assez de didactique la notion de raisonnement modulo une certaine équivalence. Ce qui rend lourd les preuves formelles axiomatiques, c'est en partie la nécessité d'appliquer une foule d'axiomes de transformations arithmétiques. Les techniques de preuves en théorie des types d'ordre supérieur procèdent modulo la β-conversion, ce qui évacue une partie des équivalences. Ici, un petit bémol : en pratique, il est souvent assez pénible de raisonner avec Coq dans des structures quotientées par un isomorphisme, parce que deux termes isomorphes ne sont pas β-équivalents. Enfin bon, tout ceci dépasse le propos du livre.

Je serais par contre plus réservé en ce qui concerne les interprétations physiques de la thèse de Church. Pour tout dire, elles me paraissent trop spéculatives à mon goût.

Cet ouvrage a une orientation claire, sinon grand public, du moins envers un public plus familier de philosophie et de sciences humaines que des mathématiques. On n'y trouvera pas de preuve de la normalisation forte du système F, ni d'explications détaillées sur le théorème de Gödel. Ce n'est pas un cours de master 2 d'informatique...