Thierry Coquand prononce sa leçon inaugurale au Collège de France
Invité pour l’année 2024-2025 sur la chaire Informatique et sciences numériques créée en partenariat avec Inria, Thierry Coquand, mathématicien et professeur d’informatique à l’université de Göteborg, en Suède, a prononcé sa leçon inaugurale intitulée « La théorie des types, de Russell aux assistants à la démonstration », au Collège de France le 13 mars 2025. Coquand, partisan de la philosophie constructiviste en mathématiques, a introduit le concept de calcul des constructions, qui est à la base de logiciels d’assistant de preuve tels que Coq et Lean, permettant de représenter et de vérifier des preuves mathématiques sur ordinateur.
Les mathématiques, souvent perçues comme une discipline complexe, fascinent à la fois élèves et chercheurs. Thierry Coquand souligne l’importance de comprendre les mécanismes sous-jacents aux démonstrations mathématiques, notamment en ce qui concerne les preuves non constructives, qui posent des défis à la compréhension intuitive.
Historiquement, les mathématiques ont été définies comme une vérité universelle, mais cette vision est débattue. Le constructivisme, qui stipule qu’un objet ne peut être prouvé existant que s’il peut être construit, a été un sujet de controverse parmi des mathématiciens de renom au début du XXe siècle. Ce débat inclut des figures telles que David Hilbert et L.E.J. Brouwer, qui ont exploré des concepts comme l’axiome du choix et le principe du tiers exclu.
Au cours des années 1980, un rapprochement entre mathématiques et informatique a vu le jour, notamment avec la programmation fonctionnelle, qui repose sur le lambda-calcul. Coquand a travaillé sur un formalisme unifiant les preuves mathématiques et la programmation, introduisant le calcul des constructions. Ce travail a attiré l’attention de Vladimir Voevodsky, qui a découvert que ce formalisme possédait une sémantique naturelle liée à la théorie de l’homotopie.
Un des résultats de ce formalisme est le développement de logiciels comme Coq, maintenant appelé Rocq, et Lean, qui aident à la vérification des preuves mathématiques. Ces outils sont essentiels pour les chercheurs souhaitant prouver des systèmes complexes, notamment en informatique.
Les défis dans ce domaine incluent la représentation de concepts fondamentaux comme l’égalité, une question qui a occupé Coquand pendant près de trente ans. Sa collaboration avec Voevodsky a permis de surmonter certaines de ces difficultés en intégrant des connaissances issues de différents domaines mathématiques.
Pour l’année 2024-2025, Coquand, en tant que titulaire de la chaire annuelle du Collège de France, se sent responsable de la promotion des mathématiques constructivistes et se réjouit de partager les avancées et les défis de ce domaine.
Source : Collège de France
