Colloquium en 2022
La ``théorie de la démonstration’’ est une branche de la logique mathématique apparue vers 1930 avec les travaux de Arendt Heyting, Andreï Kolmogorov, et surtout Gerhard Gentzen qui en 1934 propose une formalisation des preuves mathématiques qu’il appelle ``calcul des séquents’’. En 1980, William Howard remarque qu’un certain lambda-calcul typé est identique, aux notation près, au formalisme de Gentzen. Cette remarque, maintenant connue sous le nom d’``Isomorphisme de Curry-Howard’’, a enthousiasmé nombre d’informaticiens théoriciens, ce qui a donné lieu à des théories de fondation des mathématiques, comme par exemple la théorie des types de Per Martin-Löf, et à la création d’assistants de preuves, comme par exemple COQ. Dans les années qui ont suivi, on s’est aperçu que cela posait certains problèmes. Par exemple, Martin-Löf explique dans un article publié en 2006 que sa théorie de 1984 est problématique, et le système COQ a dû être amendé le jour où on s’est aperçu qu’un certain théorème de Radu Diaconescu n’était pas démontrable dans le système. Ces mésaventures sont la conséquence du fait qu’on a (sans doute plus ou moins inconsciemment) admis que le formalisme de Gentzen représentait bien les preuves mathématiques telles qu’on les pratique tous les jours, ce qui ne peut être qu’un postulat. C’est pour ces raisons que je me suis demandé s’il pouvait exister une méthode qui nous conduirait à la structure des preuves sans qu’on ait besoin de s’appuyer sur un postulat. L’entreprise peut paraître désespérée, mais cette méthode existe bien, et c’est elle qui est le sujet de cet exposé. L’exposé reste élémentaire, ne supposant que des notions mathématiques standard (niveau L1), et la compréhension de la dichotomie signifiant/signifié que j’expliquerai.
Je présenterai des exemples de modèles mathématiques de systèmes sociaux, tirés de mon livre « Pourquoi la société ne se laisse pas mettre en équations » (Seuil, 2018). Je soutiendrai que, bien qu’ils puissent être conceptuellement utiles pour corriger nos modèles intuitifs de mécanismes sociaux, leur pertinence pour les systèmes sociaux réels n’est pas évidente. Qui plus est, puisque les physiciens ont toujours eu besoin de « dompter » le monde à l’intérieur des laboratoires pour rendre leurs modèles pertinents, la modélisation sociale est liée au « dressage » des humains.
L’histoire des nombres a le plus souvent été sous la forme de chapitres attachés à des « peuples » ou des « civilisations ». L’exposé vise à expliquer de quelles hypothèses tacites ces histoires sont le fruit et à donner quelques raisons d’en mettre en doute le bien-fondé. Nous verrons qu’il convient de distinguer entre divers types de signes numériques et de réintroduire le calcul au cœur de toute histoire des nombres.
L’un des objets de la théorie ergodique est de décrire la statistique suivie par l’essentiel des orbites d’un système dynamique donné. Pour des systèmes « chaotiques » (que les dynamiciens préfèrent généralement appeler systèmes hyperboliques), cette étude passe souvent par l’utilisation de certains feuilletages dynamiquement définis. Dans cet exposé, je rappellerai les propriétés de base de ces feuilletages, et comment ces objets géométriques interagissent avec certaines mesures invariantes spécialement importantes, permettant de décrire le comportement statistique d’un « gros » ensemble d’orbites. Si le temps le permet, je parlerai d’un résultat récent obtenu en collaboration avec S. Alvarez, D. Obata et B. Santiago sur la rigidité de ces mesures dans le cas de systèmes hyperboliques sur le tore .