Mathématicien et professeur d’informatique à l’université de Göteborg, en Suède, Thierry Coquand est partisan de la philosophie constructiviste en mathématiques. Il a introduit la notion de calcul des constructions, sur laquelle se fondent des logiciels d’assistant de preuve comme Coq et Lean, qui permettent de représenter et de vérifier des preuves mathématiques sur ordinateur.
Il est invité à occuper pour l’année 2024-2025 la chaire Informatique et sciences numériques, créée en partenariat avec Inria.
Némésis de certains élèves et révélation pour d’autres, les mathématiques fascinent autant qu’elles peuvent paraître impénétrables. Chaque raisonnement mathématique, aussi complexe soit-il, peut pourtant se décomposer en parties plus simples qui aident à le comprendre. C’est ce constat, et l’aura mystérieuse qui nimbe cette discipline scientifique, qui a capturé l’intérêt de Thierry Coquand, aujourd’hui mathématicien et professeur en informatique à l’université de Göteborg en Suède, dès ses années de collège. « Ce qui me fascine, c’est de comprendre ce qu’il se passe quand on démontre quelque chose, explique-t-il. En mathématiques, certaines preuves, dites non constructives, semblent magiques en montrant l’existence d’un élément sans le construire effectivement, mais quand on assiste à un tour de magie, on a envie de comprendre l’astuce sous-jacente, et c’est ça qui motive, je pense, les mathématiciens constructivistes. »
Classiquement, et depuis des penseurs comme Aristote ou Platon, les mathématiques sont définies comme une forme de vérité absolue et universelle, antérieure et extérieure à leur perception par l’homme. Mais tous les mathématiciens ne s’accordent pas sur cette définition, et certains pensent que les mathématiques, comme un langage, sont un produit de l’esprit humain. La philosophie constructiviste est de cette approche, et stipule que l’existence d’un objet ne peut être démontrée que si l’on peut établir une construction mentale de ce dernier, c’est-à-dire une suite d’opérations qui l’exhibe effectivement. Au début du XXe siècle, cette philosophie fait grand débat, entre des mathématiciens de renom comme David Hilbert, L.E.J. Brouwer ou encore Henri Poincaré. L’un des points soulevés est le problème de l’axiome du choix et le principe du tiers exclu, qui permettent de telles preuves d’existence non effectives. D’après ce principe, soit une proposition est vraie, soit sa négation est vraie, et il n’existe pas de tierce option. En somme : A est vrai ou faux ; Aristote est vivant ou mort, par exemple. Pour L.E.J. Brouwer, ce principe ne se vérifie pas systématiquement en mathématiques et implique des notions non intuitives. Cependant, les constructivistes aspirent à une science mathématique qui renoue avec l’intuition, et dont les démonstrations sont ancrées dans une telle logique palpable. « Pour moi, les mathématiques qui se passent du tiers exclu sont bien plus élégantes, mais tous ne sont pas de cet avis », précise Thierry Coquand, qui a surtout travaillé en algèbre et réussi, avec Henri Lombardi et Claude Quitté, à expliquer plusieurs preuves non effectives d’existence d’objets concrets dans ce domaine. « On essaie de comprendre où se trouvent de tels objets dans une preuve mathématique, et à chaque fois qu’on essaie de le déterminer, on a l’impression de mieux comprendre la preuve elle-même. »
Entre mathématiques et informatique
Dans les années 1980 s’opérait un grand rapprochement entre les travaux de certains informaticiens et des problèmes de logique mathématique. « Ce que l’on appelle aujourd’hui la programmation fonctionnelle était en plein développement, explique Thierry Coquand. Et celle-ci se fonde sur le lambda-calcul, un langage de programmation théorique inventé dans les années 1930 par le logicien américain Alonzo Church. » À cette époque, le mathématicien hollandais Nicolaas de Bruijn cherchait à comprendre comment représenter les mathématiques sur ordinateur, notamment en mettant au point un système capable de vérifier les preuves. Il a alors mis au point un formalisme – un système composé d’un langage et d’une sémantique visant à représenter un objet d’étude de manière non ambiguë – nommé « type dépendant ». Fondé sur le lambda-calcul, ce formalisme a des connexions fortes avec les mathématiques constructives et est très similaire au formalisme parallèlement étudié par des logiciens, comme le Français Jean-Yves Girard. Ancien élève de l’École normale supérieure, Thierry Coquand arrive dans ce contexte et travaille pour sa thèse en 1985 à dresser une synthèse de ces différentes sortes de lambda-calcul. « Comme il y avait un rapprochement avec la programmation fonctionnelle, je voulais mettre au point un formalisme qui unifie, et qui pourrait être utilisé à la fois pour établir des preuves mathématiques et écrire des programmes », se rappelle-t-il. Il effectue ce travail sous la direction de Gérard Huet, spécialiste de la programmation fonctionnelle et des preuves sur machine, et introduit avec lui la notion de calcul des constructions.
Ce nouveau formalisme est alors encore un peu trop formel, et ne semble pas posséder de sémantique claire, mais il attire l’attention d’un grand mathématicien russo-américain, Vladimir Voevodsky, qui cherche lui aussi à représenter les mathématiques sur ordinateur. Alors que ce dernier écume les systèmes dans lesquels sont représentées les preuves mathématiques, il tombe sur ce formalisme des types dépendants et se prend de fascination pour lui. En se penchant longuement sur la question, il se rend compte que le formalisme a bel et bien une sémantique naturelle, provenant précisément de son domaine de travail : la théorie de l’homotopie, sorte d’étude abstraite des formes en mathématiques. Vladimir Voevodsky commence donc à établir des preuves dans ce formalisme, afin de vérifier sa pertinence pour représenter des notions mathématiques de manière satisfaisante. Dans ce cadre, il organise à l’Institut d’études avancées de Princeton une année de recherche consacrée à ce problème en 2012-2013. « Cette expérience a attiré beaucoup de jeunes chercheurs en mathématiques et en informatique », remarque Thierry Coquand, qui s’était rendu à Princeton pour coordonner le projet avec son collègue russo-américain. « Elle a donné lieu à un dialogue très vivant et excitant visant à comprendre le rapport entre, d’un côté, ce formalisme qui essayait de représenter des preuves sur machines et, de l’autre, la théorie de l’homotopie. Les recherches sur le sujet se poursuivent maintenant depuis plus de dix ans, grâce à de jeunes chercheurs qui arrivent à raisonner directement dans ce cadre de pensée, d’une manière qui était impensable il y a seulement vingt ans. J’ignore où cela va nous mener, mais c’est très intéressant et met en lumière cette connexion forte qui existe entre ces différents domaines mathématiques. »
Un logiciel pour vérifier les preuves
Un autre résultat du formalisme établi par Thierry Coquand est le développement d’un logiciel baptisé « Coq », par une équipe de l’Inria et, plus récemment, du logiciel Lean développé aux États-Unis. Il s’agit d’un assistant de preuve dont la logique repose sur le calcul des constructions et dont l’objectif est d’aider mathématiciens et informaticiens à vérifier des preuves mathématiques. Le principe est simple : l’utilisateur interagit avec le système en formulant un énoncé mathématique et sa preuve, puis le système vérifie que l’énoncé est bien formulé, et vérifie ensuite la correction de cette preuve. C’est un outil précieux pour les chercheurs qui veulent prouver des systèmes ou certains programmes, comme des compilateurs. Il est aussi utile dans la théorie des langages de programmation pour mettre au point ces langages et montrer qu’ils se fondent sur les bonnes propriétés.
En mathématiques, les preuves sont souvent de plus en plus longues, et certains mathématiciens s’étaient rendu compte que des résultats sont parfois si compliqués que personne ne les vérifie vraiment. Vladimir Voevodsky avait présenté l’un de ses résultats en exposé à plusieurs reprises, puis, lors d’un nouvel exposé plus détaillé, il a remarqué que la preuve qu’il donnait et le résultat qui en découlait étaient faux, alors que celui-ci était déjà cité et utilisé par d’autres mathématiciens. Ce constat l’a amené à réaliser que d’autres résultats de son domaine, longtemps pensés corrects, ne l’étaient pas. Or, en mathématiques, certains s’attaquent à des problèmes ouverts en fondant leurs réflexions et leurs travaux sur des résultats établis précédemment. Il s’agit parfois de longs efforts, échelonnés sur plusieurs années. « Alors, quand la preuve utilisée comme fondement se révèle fausse après un examen détaillé, c’est vraiment terrible, déplore Thierry Coquand. » Ce problème de confiance a rendu difficiles les collaborations entre de nombreuses personnes, car les résultats ne peuvent pas être utilisés avec le même degré de certitude absolue que, par exemple, des boîtes noires. Heureusement, grâce aux assistants de preuve comme les logiciels Coq ou Lean, les travaux collaboratifs entre mathématiciens pourront de nouveau avoir le vent en poupe. « On peut lancer des problèmes qui peuvent être étudiés par des vingtaines de personnes dans le monde, se réjouit Thierry Coquand. Et on sera sûrs de la correction, car leur résultat sera vérifié par l’assistant de correction. C’est ce qui est en train de se passer de plus en plus. » Idéalement, et à terme, ces logiciels devraient être capables de faire encore plus que cela ; en aidant notamment les chercheurs à trouver des preuves, en plus de les vérifier.
Les défis des mathématiques
L’une des grandes difficultés rencontrées par Thierry Coquand dans l’établissement de son formalisme fut de représenter une notion, pourtant élémentaire dans les mathématiques : l’égalité. Une difficulté qui l’a tenu en haleine pendant près de trente ans. Si ce formalisme parvenait bien à représenter des mathématiques assez concrètes, comme la théorie des graphes ou des groupes finis, il n’arrivait pas à représenter ses penchants plus abstraits, tels que l’analyse ou la théorie des catégories. C’est en collaborant avec Vladimir Voevodsky, issu d’un domaine mathématique différent, que la situation s’est finalement débloquée. « Grâce à notre dialogue, je me suis rendu compte qu’il fallait connaître des choses comme la théorie de l’homotopie pour comprendre l’égalité dans ce formalisme, relate Thierry Coquand. Cela montre qu’il faut une véritable capacité de transversalité pour surmonter les problèmes, et s’ouvrir à d’autres domaines de mathématiques, desquels nous ne sommes nous-mêmes pas spécialistes. Cela m’amène à apprendre quelque chose de nouveau et de totalement captivant. »
Pour l’année 2024-2025, Thierry Coquand est titulaire de la chaire annuelle du Collège de France Informatique et sciences numériques, une nomination qu’il reçoit avec beaucoup d’humilité et d’intérêt. C’est l’occasion pour lui de réfléchir à ce qu’il est important d’aborder dans sa discipline, parfois difficile à représenter auprès d’une audience assez large. « Je me sens responsable, en quelque sorte, du domaine des mathématiques constructivistes, à l’occasion de ces cours, mais je me réjouis de présenter les tenants et aboutissants du domaine, et les problèmes qu’il reste à résoudre ! » Une occasion, peut-être, d’inspirer de potentiels jeunes chercheurs comme il l’a déjà fait dix ans plus tôt lors de l’année spéciale organisée à l’Institut d’études avancées de Princeton.
Article de William Rowe-Pirra
