Hier, à l'Institut Henri Poincaré avait lieu le colloque de lancement d'un trimestre thématique| sur les liens entre théorie de la preuve, informatique (preuve de programmes) et mathématiques (preuves formelles de théorèmes).

L'assistance était assez guindée : il y a avait aux moins deux médaillés Fields (Cédric Villani et Vladimir Voevodsky), d'augustes mathématiciens (Pierre Cartier, Jean-Yves Girard, Per Martin-Löf...), des informaticiens distingués (Christine Paulin-Mohring, Xavier Leroy, Gérard Huet...) — et bien entendu quelques humbles marmottes, dont David Madore et votre serviteur. L'amphi Hermite (bancs et tables étroites à l'ancienne) était d'ailleurs plein à craquer.

Les trois premiers exposés m'ont donné des impressions de déjà vu (ce qui n'est pas étonnant), mais j'attendais beaucoup de l'exposé de Voevodsky sur les fondations univalentes, tout simplement parce que j'entends beaucoup parler de ce thème de recherche et que je n'y comprends rien (je pense savoir vaguement que cela vise à régler la question de l'égalité de façon plus satisfaisante ; tous ceux qui ont fait du Coq savent bien combien il est pénible de raisonner modulo isomorphisme ou quotientage, même si la situation s'est beaucoup améliorée ces dernières années).

Hélas, l'exposé était totalement décousu, commençant par quelques points incompréhensibles sur les ω-groupoïdes (je ne sais pas ce que c'est) et se terminant par un rant sur le fait qu'il faudrait admettre (au moins à titre de possibilité optionnelle) les termes qui ne terminent pas et Type:Type (oui, devant Martin-Löf et Girard !) (*). Il a fini par dire (certes en souriant) qu'il croyait incohérente l'arithmétique de Péano... (**)

Quel trolleur !

(*) De fait, Coq se comporte superficiellement comme si Type:Type, mais met en fait en œuvre une infinité dénombrable d'univers avec des contraintes de compatibilité. Ouf, nous sommes sauvés.

(**) Dans mes souvenirs, il disait qu'il ne la croyait pas cohérente, mais D. Madore m'indique avoir clairement entendu qu'il la croyait incohérente. Je n'ai pas vérifié avec la vidéo.