Une coquille semble-t-il : au lieu de « Le formalisme de la théorie des types constitue une alternative à la théorie des types » il faut lire « Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles »

Si je puis me permettre : « Le formalisme de la théorie des types constitue une alternative à la théorie des types pour décrire les fondements des mathématiques. » devrait plutôt être : « Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles pour décrire les fondements des mathématiques. »

Merci d’avoir attiré l’attention sur ce livre, par votre bel et clair article !

Une remarque concernant les preuves automatiques et votre commentaire louangeur concernant « des logiciels de vérification de preuve, tels que Coq (initialement issu du Calculus of Constructions de Thierry Coquand) qui ont récemment eu de jolis succès en permettant la vérification par Georges Gonthier et son équipe du théorème des 4 couleurs ou du théorème de Feit-Thompson » :

. combien de pages pour ces démonstration ?

. sont-elles lisibles ? combien de millions d’inférences ?

. qui peut les relire.

. qui a démontré le démonstrateur ? lui-même ? un autre ?

En conclusion, peut-on encore parler de démonstrations donc de preuves ?

Je n’ai pas regardé les vérifications de l’équipe de Gonthier, mais j’avais jeté un œil au livre de Thomas Hales (Dense sphere packings — A blueprint for formal proofs), qui est assez lisible (c’est, si je puis dire, une traduction en langage usuel de la preuve formelle). De fait, ainsi qu’explique Hales (par exemple dans son article « Mathematics in the Age of the Turing Machine »), les preuves formalisées ne sont guère plus longues que les preuves originelles.)

Enfin, les logiciels de vérifications de preuves ont un noyau initial très petit qu’on peut vérifier facilement, et le reste est fait de proche en proche (un peu comme les compilateurs des langages modernes).

Enfin, entre des dizaines de pages d’études de cas, et une description formelle des calculs qu’il faut mener, jointe au résultat de leur vérification mécanisée, je vous laisse juge de ce qui est le plus sûr.

Toutefois, vérifier informatiquement une preuve n’améliore a priori pas la compréhension des mathématiques (à moins que pour ne faire cette vérification, on n’ait été amené à penser différemment la preuve que l’on vérifie). Cette dernière assertion doit être bémolisée : dans le livre dont cette chronique est l’objet, de nombreuses preuves ont d’abord été menées à l’aide du logiciel de vérification de preuve (qui mérite dans ce cas son nom d’« assistant de preuves »).

On peut signaler aussi que la théorie des catégories, qui est très générique, trouve des applications dans d’autres domaines tels que la linguistique (grammaires catégorielles) et la physique. Un formalisme simple permet déjà d’effectuer des traitements sophistiqués.

Olivier

Merci à Antoine Chambert-Loir pour cette très bonne introduction. Je me permets d’ajouter pour répondre à certaines inquiétudes que l’avantage de la théorie des types et en particulier de la théorie des types avec l’axiome d’univalence est qu’elle permet des preuves formelles qui sont de tailles tout à fait comparables aux preuves informelles (évidemment des preuves informelles comme dans la pratique courante des mathématiciens sont aussi possibles, c’est d’ailleurs le choix de présentation du livre mentionné) et qui restent relativement compréhensibles. Evidemment rien n’interdit en théorie des ensembles, disons ZFC, des preuves formelles mais celles-ci deviennent vite incompréhensibles même aux mathématiciens chevronnés et sont d’une complexité qui explose très vite. Cette mise au pas de la formalisation et l’absence d’énoncés
sans sens sont donc deux avantages des fondations univalentes qui ressortent bien de l’article de monsieur Chambert-Loir.

Le séminaire Bourbaki de juin 2014 met la théorie homotopique des types et la preuve formelle au programme : un exposé de Thierry Coquand sur Théorie des types dépendants et axiome d’univalence et un de Thomas Hales sur Developments in formal proofs.