Entretien avec Hugo Herbelin et Paul-André Melliès, directeurs de recherche INRIA à l'IRIF, qui ont obtenu un financement pour leur projet ERC Synergie

Hugo Herbelin, Carlos Simpson, Paul-André Melliès et Philippe de Groote

Pour Hugo Herbelin et Paul-André Melliès, le chiffre 4 semble être un porte-bonheur : pendant 4 ans, c'est à 4 qu'ils ont construit leur projet pour finalement obtenir leur bourse Synergie du programme de recherche européen. Avec Philippe de Groote et Carlos Simpson, la langue naturelle mathématique n'aura plus de secret. Rencontre et échanges avec Hugo Herbelin et Paul-André Melliès, directeurs de recherche INRIA, porteurs du projet MALINCA.

“Avec notre ERC, nous espérons pouvoir comprendre comment, à l'intérieur d'un texte mathématique (que l'on peut trouver dans un article, dans une page de livre de maths), qui est écrit dans ce que l'on appelle une langue naturelle (anglais, français, etc.), le texte contient en lui-même les éléments de sa correction mathématique.”

Il y a 5 ans, nous avons découvert l'existence de cette ERC Synergie. Auparavant, nous avions en tête que les ERC s'assimilaient à un exercice solitaire de la recherche, par lequel les chercheurs et chercheuses pouvaient vouloir passer à un moment de leur carrière.

Quand nous avons pris connaissance de l'existence de l'appel à projet pour la bourse ERC Synergie, nous avons commencé à échanger, d'abord entre nous [Paul-André Melliès et Hugo Herbelin], dans le couloir de l'IRIF, au 3e étage du bâtiment Sophie Germain. Nous nous disions que cette bourse était le moyen de faire quelque chose d’original, d'ambitieux, et de novateur, qui dépasse ce qu'il nous aurait été possible de faire seuls. De plus, cet aspect synergétique nous plaisait car il correspondait beaucoup plus à la manière dont nous souhaitions fonctionner, en réseau et au niveau européen.

Nous avons soumis ce projet trois fois avant qu'il ne soit accepté, ce qui l'a fait considérablement évoluer et nous a aidé à le faire arriver à maturité. Ces quatre années ont donc été vraiment déterminantes pour la construction de notre projet et nous n'imaginions pas que tout ce temps serait nécessaire pour arriver à en définir aussi solidement les bases. Au-delà du souhait de voir le projet accepté, ce qui nous a motivé était que nous nous rencontrions, portés par un désir scientifique fort et partagé. Le travail mené ensemble ne nous a jamais semblé inutile, bien au contraire, puisque nous avons fait évoluer la science pendant ces quatre années. L'INRIA a également joué un rôle important dans le sens où nous avons pu intégrer plusieurs éléments du projet en ébauche dans les objectifs de l'équipe Picube. Nous avons aussi bénéficié des ressources de l'Université Paris Cité à travers le projet Aprapram mené avec Riccardo Brasca et Antoine Chambert-Loir de l'IMJ-PRG.

Travailler de manière collective en Synergie nous a aussi permis de mieux vivre le fait que le projet a été soumis trois fois sans être retenu, et nous concentrer sur les discussions et la dynamique scientifique du projet.

Cette ERC s’est construite autour la rencontre de quatre chercheurs.

Hugo, dans son travail de recherche, s'attache à développer des systèmes qui permettent de traduire des textes mathématiques pour avoir des preuves formelles que l'ordinateur comprends.

La première personne à qui nous avons pensé lorsque l’on a échangé est Philippe de Groote, qui a beaucoup réfléchi à la structure de la langue en lien avec des outils que nous connaissons bien, de la théorie des types, qui est le formalisme logique que l'on utilise dans les systèmes comme Rocq, anciennement appelé Coq. Philippe a été pionnier dans l'étude des liens entre langues naturelles et théorie des types, en s'appuyant sur une tradition qu'il a beaucoup fait avancer.

Avec notre ERC, nous espérons pouvoir comprendre comment, à l'intérieur d'un texte mathématique (que l'on peut trouver dans un article, dans une page de livre de maths), qui est écrit dans ce que l'on appelle une langue naturelle (anglais, français, etc.), le texte contient en lui-même les éléments de sa correction mathématique.

Historiquement, ce qui est fait théoriquement depuis les années 1930 et technologiquement depuis 1970, c'est que pour vérifier la correction logique d'un texte mathématique, il faut d'abord le traduire dans une langue qui est une langue formelle, avec des formalismes logiques. Il y en a différents types, comme par exemple la théorie des ensembles et la théorie des types, très populaires aujourd'hui, notamment à l'IRIF. Cette idée est historique et dessus, reposent des systèmes comme Coq, Agda, Lean, par exemple, qui tentent de prouver les mathématiques.

Il y a une traduction qui est faite, ou comme le dit si bien Philippe de Groote, une manufacture des textes mathématiques pour les transformer dans une langue que l'ordinateur peut comprendre.

La deuxième personne qui s'est imposée à nous est Carlos Simpson, un mathématicien hors pair, pionnier dans la formalisation des mathématiques dans Rocq. Il est notamment le premier à s’être spécialisé sur les formes de théories algébriques, dont la théorie des faisceaux et leur formalisation. Il continue de mener ce travail depuis la fin des années 90, avec un autre chercheur à Nice, André Hirschowitz, sur la formalisation et l'enseignement des mathématiques en stylisant le système Rocq. Il a également un point de vue très intéressant sur les mathématiques, parce qu’il considère que de manière générale, elles ne sont pas suffisamment écrites. Selon lui, des idées mathématiques sont échangées sans que les arguments ne soient complètement développés, puisque ça prendrait trop de temps. Ce sont les mathématiciens qui s'accordent à dire que telles idées sont validées et correctes, ce qui peut entraîner des effets stylistiques d'autorité. Par conséquent, il y a une vraie réflexion sur la transmission de la vérité et des idées mathématiques.

Aujourd'hui, l'utilisation de systèmes comme Lean ou Rocq reste relativement marginale dans la pratique des mathématiques, qui repose essentiellement sur de la langue naturelle. Toutes les mathématiques jusqu'à aujourd'hui reposent sur des validations qui passent par des rapporteurs humains, ce qui peut poser des problèmes et un questionnement sur la pérennité du modèle : sommes-nous toujours capables de fabriquer des mathématiques avec les chercheurs et chercheuses qui sont poussé-e-s à produire de plus en plus de travaux ?

Les rapporteurs passent moins de temps sur les articles. Un essai parle justement du défaut de qualité d'évaluation du travail mathématique, à une période où les mathématiques deviennent de plus en plus sophistiquées. Les jeunes thésard-e-s sont lancé-e-s sur des sujets reposant sur des résultats supposés corrects mais comme ils n'ont pas le temps de regarder la preuve, ils s'appuient sur les résultats eux-mêmes, sans faire de vérification. C'est bien évidemment un travail dantesque pour la communauté que de relire les articles importants, d'essayer de les réécrire mais malgré tout, la transmission repose sur la langue naturelle.

A notre niveau, nous nous inscrivons dans la tradition de la langue ; depuis de nombreuses années nous participons au développement du système Rocq. Cette tradition repose sur l'idée de manufacturer, de traduire des textes de la langue naturelle vers une langue plus formelle. Or, avec les nouvelles idées mises en place du côté de la linguistique, nous pouvons essayer de repenser cette articulation entre naturel et formel.

C'est en cela qu'existe notre projet : nous comparons le discours mathématique avec d'autres formes de discours. Il y a en particulier des formes d'analyse syntaxique, comme la structure grammaticale d'un texte. En le structurant, nous nous demandons quelles sont les unités de discours qui communiquent avec d'autres à l'intérieur même d'un texte en langue naturelle.

De plus, nous nous appuierons sur quelque chose de très particulier de la langue mathématique, le référent : les mathématiciens l’utilisent lorsqu'ils échangent. Ce référent est lié à leur pratique mais il y a aussi l'idée que malgré tout, souvent, derrière le discours mathématique, il y a un discours de vérité. Il serait intrinsèquement particulier dans l'univers, dans l'espace global de la langue. Il y aurait, à l'intérieur de cet espace linguistique, un fragment de langue mathématique, qui a ses propres propriétés, mais qui est censé, lorsqu'on la pratique, décrire les objets de manière excessivement univoque.

Lorsque nous avons échangé avec Carlos Simpson, il s'intéressait plus particulièrement au machine mearning pour les mathématiques. Nous le contactions un peu par “hasard” en tant que mathématicien qui faisait de la formalisation et le machine learning s'est ajouté comme une nouvelle corde à son arc, d'autant plus importante et précieuse pour notre projet.

Via notre ERC, nous souhaitons comprendre les structures linguistiques de notre problème synergétique, donc comprendre les structures linguistiques d'un texte mathématique et comment ces structures linguistiques produisent le sens : le code des mathématiques est quelque part déjà inscrit dans la langue naturelle [ultimate code dans les transparents]. Cette phrase est importante car elle dit que seul le texte échangé suffit et qu'à partir de ce texte nous devrions pouvoir ensuite élaborer et comprendre l'ensemble de la signification mathématique.

Nous espérons qu'une machine sera capable de le faire ; elle devrait s'appuyer sur une vraie réflexion de nature conceptuelle sur la place de la langue mathématique à l'intérieur de la globalité de la langue naturelle. En somme, il y a des choses que l'on ne peut pas faire dans la langue naturelle et que l'on espère pouvoir faire dans la langue mathématique, parce qu'elle se veut univoque.

Notre projet a aujourd’hui évolué, nous allons dans un sens qui n'était pas du tout évident il y a quatre ans, celui de la langue naturelle. Il y a une tentation de dire que, une fois que l'on sait manufacturer un texte mathématique pour le transformer en code, il n'y a qu'à le faire. Il y a des experts de ce travail, qui essaient également d'améliorer les systèmes. Notre projet, de partir de la langue naturelle est un travail très ambitieux, à travers lequel nous devons réfléchir aux outils que l'on va et doit utiliser. Et dans ce cadre-là, la bourse Synergie prend tout son sens, parce nous allons pouvoir discuter avec des linguistes de leurs intérêts et leurs pratiques. Nous avons beaucoup appris de la pratique justement apportée par Philippe de Groote : chaque phrase d'un texte doit être lue très attentivement, puis il faut en faire une analyse philologique. Ce n'est pas ce que l'on fait habituellement lorsque l'on fait des mathématiques formalisées.

Ceci s'inscrit dans un phénomène mondial qui fait que les chercheurs souhaitent faire de plus en plus de mathématiques dans des assistants à la démonstration ou à la preuve.

Tout d'abord, le langage naturel s'oppose au langage formel. A cela s'ajoute plusieurs gradations : le langage naturel, c’est celui avec lequel on écrit par exemple sur le tableau noir, puis il y a un langage plus formalisé (qui reste une langue naturelle) quand on écrit un article, puisqu’on essaie d'écrire avec plus de rigueur. Progressivement, on arrive à une langue compréhensible par la machine. C'est l'objectif de notre projet : partir d'une langue naturelle suffisamment bien écrite, pour qu'elle soit comprise mais surtout validée par l'ordinateur. Pour valider la correction, il faut la comprendre, dans le sens de la théorie des types.

Nous partons d’un fragment de la langue naturelle globale, à l'intérieur de laquelle se trouve la langue mathématique. Elle pourra être traduite, puisqu’elle est faite en quelque sorte pour transmettre une information, de nature univoque, et donc transmettre un discours de vérité, sur des objets pour lesquels on considère que nous avons une description précise. Il peut néanmoins y avoir différentes descriptions équivalentes d’un même objet mathématique et on peut tenir des discours similaires comme par exemple avec les réels, qui sont un objet mathématique de base aux nombreuses définitions. Pourtant, bien qu'il y en ait plusieurs, elles sont équivalentes à un certain niveau et les discours que les mathématiciens tiennent au sujet des réels ne dépendent pas moralement de la définition, puisqu'elles sont équivalentes. Cela pose donc des questions linguistiques qui sont difficiles et importantes.

Notre postulat est qu'à l'intérieur de la langue naturelle mathématique, nous allons pouvoir faire des choses que nous ne pouvons pas faire dans la langue naturelle générale, qui est beaucoup plus équivoque, la transmission du sens étant compliquée à traiter. Du point de vue de la linguistique, traité notamment par Philippe de Groote, c'est une notion importante.

Nous faisons le pari que le sous ensemble mathématique de la langue naturelle est en fait bien délimité. C'est à dire que nous avons l'illusion que parce que la langue naturelle mathématique est de la langue naturelle, qu'elle est arbitrairement complexe. Néanmoins, même si elle a une apparence de liberté complète des mots, elle a une structure et un contour logique et ceci même si ce contour logique peut-être sophistiqué : par exemple, la langue mathématique est aussi capable de s'auto-référencer avec des méthodes de preuves du genre : « en prenant la preuve du paragraphe précédent, remplacez X par Y » et vous obtenez une autre preuve pour prouver un autre théorème. Ce sont des choses que l'on s’autorise et nous espérons pouvoir mécaniser concrètement ce genre de choses, d'en faire une liste à peu près exhaustive. A partir de celle-ci, nous pourrons construire une grammaire de la langue naturelle mathématique.

Nous avons une garantie d'exhaustivité parce que l'on s'est restreint aux tournures mathématiques présentes dans cinq livres que l'on a choisi et qui sont donc en nombre fini. Pour procéder, nous appliquons en fait des méthodes de linguistique, et c'est là que la Synergie prend tout son sens, puisque nous avons désormais la possibilité de comprendre de manière exhaustive ce qu'il se trouve dans ces cinq livres. Nous souhaitons construire un bon usage de la langue mathématique.

Ce qu'il y a d'exceptionnel avec les mathématiques, c'est qu'elles peuvent se pratiquer dans toutes les langues. Contrairement à de la poésie par exemple, si on veut la traduire dans une autre langue, c'est un nouvel exercice de poésie. Quand on traduit un texte mathématique, on peut considérer que le sens fondamental a bien été reflété. Le fait de pouvoir échanger sur les mathématiques, dans toutes les langues peut donner l'impression de parler d'autre chose que de la langue, comme de parler d'idées, d'intuitions, qui sont néanmoins transmises par la langue.

En particulier, les conditions de vérité du discours mathématique seraient dans la langue. C'est la question que nous nous posons, qui est presque un pari dans le cadre de notre recherche. Nous cherchons en fait à comprendre ce qui fait qu'une preuve mathématique est correcte dans sa forme ainsi que dans son fond.

Tout texte mathématique engendre sa propre logique. C'est un point important, car lorsqu'on lit un chapitre d'un livre par exemple, d’une certaine manière, il construit un univers mental comme un roman. On y trouve des concepts qui évoluent les uns avec les autres et on voit quelque chose apparaître. Un des éléments du projet, c'est considérer que les éléments linguistiques de celle langue-là, qui d'une certaine manière sont propres à chaque texte mathématique voire à chaque domaine mathématique, sont intéressants à étudier.

Historiquement, les scientifiques s'étaient toujours dit qu'il y avait une seule langue, celle de la logique formelle, dans laquelle tout était traduit. Ce n'est seulement une fois que l'on comprend comment chaque langue fonctionne que l'on peut la traduire. Cette traduction correspond à la vérification formelle puisque tout le monde s'est mis d'accord pour dire que la logique formelle peut servir de fondation correcte. Une question fondamentale, qui dépasse même les questions de nature mathématique, se pose : qu’est ce qui fait autorité dans une preuve et qu'on est convaincu par celle-ci ?

Carlos Simpson, lui, estime que mieux comprendre comment les mathématiques sont écrites permettra de mieux explorer des idées mathématiques avec l'aide de l'ordinateur, en utilisant des techniques du machine learning.

Pour Paul-André Melliès, il y a aussi l'idée que les mathématiques s'échangent intrinsèquement dans la langue naturelle. Quand on se demande comment sont fabriquées les mathématiques, on réalise qu'elles ne le sont pas à travers la langue formelle. Le nom d'un théorème peut avoir un effet dans le choix de l'utiliser ou non. D'un point de vue purement symbolique, les maths, par exemple, sont des symboles ; les mathématiciens font toujours très attention à bien choisir le nom des concepts, puisque c'est porteur de représentations. Cela montre bien que la langue mathématique n'est pas déconnectée de la langue naturelle. C'est un fragment qui communique à travers des imaginaires. Il y a par exemple des chercheurs qui essaient de faire de la recherche de preuve en utilisant des LLM (Large Language Models). Les mots qui sont utilisés dans les mathématiques guident justement parfois la construction mathématique.

L'importance d'un imaginaire associé aux concepts mathématiques et porté par la langue naturelle n'exclut pas de s'intéresser à la structure sous-jacentes des théorèmes.

C'est une direction que Hugo explore en parallèle. En particulier, il s'intéresse à la correspondance preuve/programme, et à comment connecter différentes branches des mathématiques qui ont leur propre culture, leur propre vocabulaire, leurs propres manières de nommer des théorèmes et leurs propres imaginaires. Mais si on regarde la structure de ces objets, c'est parfois la même que celle d'autres domaines qui développent d'autres imaginaires et d'autres terminologies, comme en particulier, faire des ponts entre l'algèbre et la géométrie ou l'informatique et la logique. S’apercevoir qu'au delà du vocabulaire il y a des structures similaires sous-jacentes est aussi une contribution que l'ordinateur peut apporter. Par ailleurs, si on prend par exemple un bout des mathématiques étudié en licence, puis d'autres plus avancés, les niveaux de complexité des concepts augmentent mais pas celui de la langue elle-même. Ce sont des unités de discours qui s'enchevêtrent les unes aux autres et qui construisent un sens. Par conséquent, ces unités de discours et ce texte mathématique en langue naturelle sont en fait une version prospective. Il n'y a pas juste une langue symbolique mais bien une langue mathématique naturelle qu'il faut analyser.

Pierre-André Melliès compare la logique au rasoir d'Ockham : c'est à dire que pour toutes les mathématiques qui se font dans nos sociétés, les différentes communautés ont développé leur propre imaginaire, leur langue, etc. Ce que dit la logique formelle dans les années 30, c'est que derrière tous ces différents groupes, derrière leurs pratiques singulières, se cache un même substrat logique, donc une langue formelle, qui permet de traduire des probabilités ou de l'algèbre, ainsi que de l'informatique fondamentale par exemple. Ce postulat a servi de base de travail à partir des années 1970, notamment pour un projet appelé Automath mené par Nicolaas Govert de Bruijn, qui a ensuite été suivi, entre autres, aux côtés de Mizar,Isabelle, NuPrl, … par le système Rocq, développé initialement par Thierry Coquand et Gérard Huet, vite rejoints par Christine Paulin-Mohring puis par Benjamin Werner et Gilles Dowek…

Les synergies linguistiques et la logique symbolique peuvent aujourd'hui être étudiées ensemble grâce aux outils qui viennent du TAL (traitement automatique des langues - NLP en anglais).

Cet ERC compte quatre chercheurs principaux mais d’autres chercheurs y participent également comme Daniela Petrişan et Benoît Crabbé (linguiste) spécialiste des TAL. Tous les deux s’intéressent beaucoup aux traductions, à la construction de codes ou de programmes Python par exemple à partir d'une description linguistique. C'est un renouveau pour les TAL, il y a une nouvelle génération d'outils comme les LLM. La mettre en vis à vis de ces outils qui viennent des TAL nous apportera la compréhension de ce qui, dans notre fond commun de la logique, peut aider à aussi s'articuler sur des nouvelles formes, qui sont des outils de probabilités et de statistiques.

L’exercice des mathématiques et de ses anciennes questions, inscrites dans la tradition de la logique symbolique puis dans celle de sa nouvelle version avec des outils issus du machine learning, participe à un mouvement, celui de comprendre les liens entre méthodes formelles et tous ces nouveaux outils. Le but n'est pas nécessairement de faire des expérimentations mais plutôt de comprendre comment les outils fonctionnent et comment les vérifier, les contrôler.

Un mouvement moderne actuel conteste que les nouveaux outils apparus récemment sont utilisés sans qu'on comprenne leurs mécanismes profonds. De la même manière, dans les années 70, il y a eu une explosion des codes informatiques ; l'IRIF est un exemple d’institut qui tente de comprendre les fondations des structures profondes de tous ces outils. C'est précisément ce qui manque aujourd'hui pour le machine learning.

Mieux comprendre comment les LLM sont capables de raisonner peut aussi nous aider à nous assurer que ces systèmes-là fonctionnent de manière plus sûre. Il y a à l’égard du *machine learning* deux approches : la première qui est le rejet, qui dit qu'il faut que ça s'arrête et qui s'oppose à l'utiliser. La seconde, qui dit que c'est impossible de ne pas regarder et l’utiliser, mais qu’il faut aujourd'hui participer à ce mouvement général qui cherche à vérifier qu'un système construit avec le machine learning ne poussera pas les utilisateurs à des comportements néfastes. En réfléchissant à la façon dont ces outils font et explorent les mathématiques, nous pourrons mieux comprendre comment ils fonctionnent grâce à une vraie méthodologie.

Les assistants à la démonstration reposent sur un travail fondamental mais également sur un savoir-faire technologique, la programmation, qui fait aussi partie des fondations. Dans l’un des aspects du projet, nous cherchons à comprendre à un niveau fondamental ce qui, historiquement, est considéré être de l’ordre de l’ingénierie, sur des questions par exemple d’élaboration, d'unification. Ils sont dans le code mais ne sont pas étudiés de manière externe.

Entres autres, l'idée est par exemple d'essayer de construire une mathématique de l'élaboration, qui est ce qui permet d'extraire le sens d'un texte mathématique (dans le sens des structures de la théorie des types). C'est une technique qui permet, lorsqu'on a écrit un texte aujourd'hui semi-formel mais qui sera en langage naturelle dans le cadre de notre ERC, de développer des techniques de parcing et d'unification. Nous voulons en faire progresser la compréhension.

Il y a un vrai travail de recherche fondamentale dans le développement logiciel d'un outil comme Rocq. Nous voulons y participer en y ajoutant la question de la langue naturelle. Et comme toute méthodologie mathématique, nous allons collecter des exemples pour trouver des généralisations, qui apporteront de nouveaux exemples et de nouvelles structures.

L'implémentation d'un système à la preuve fonctionne de la même manière : nous les expérimentons puis réalisons que certaines choses reviennent régulièrement. Ensuite, nous les conceptualisons et nous les reformulons autrement, en introduisant progressivement des couches d'abstraction intermédiaires. Dans notre ERC, nous voulons suivre cette méthodologie pour aborder la complexité de la langue naturelle ce qui n'a jusque-là jamais été tenté.

Contrairement à ce qu'on pourrait imaginer, il y a dans notre laboratoire d'informatique fondamental un vrai travail expérimental de paillasse. Le terme fondamental cache une recherche qui se fait à partir de la matière. Pour un informaticien, le travail expérimental est le développement de logiciels tel que Rocq, où il y a à la fois un travail de réflexion et d'expérimentation associé à un retour sur l'utilisation. Ce travail est souvent collectif, main dans la main entre praticiens et théoriciens. Cet exercice s'inscrit pleinement dans la culture de l'IRIF.

Il y a un réel processus historique de sophistication et d'ajout de niveaux d'abstraction dans les langages de programmation, qui déjà les rapprochent de la langue naturelle. Prenons le cas par exemple du langage fonctionnel OCaml : c'est un langage qui intègre des formes de structure mathématique, qui permet par exemple le raisonnement par récurrence de manière naturelle (par exemple : soit *f* la fonction définie par récurrence, en *0* elle vaut tant, en *n+1* elle vaut tant, etc.). Avec quelques décennies de décalage, il se passe la même chose avec les assistants à la preuve. Nous avons un langage similaire à l'assembleur, qui est la logique formelle, celle qui sert de référence pour justifier la correction mathématique dans ses diverses spécialités (l'analyse, la géométrie, …). Le système Automath utilisait justement un tel langage dans les années 60, les symboles étaient écrits un à un. Un livre entier d'analyse a été formalisé. Sur les 50 ans qui se sont écoulés depuis dans le domaine des assistants à la preuve, des niveaux d'élaboration ont été ajoutés, qui permettent désormais d'écrire les choses de manière plus fidèle à la manière dont on les pense. C’est le cas notamment des notations : on écrit *x+y* au lieu d'écrire *add x y*. On a rajouté l'élaboration, qui permet d'inférer des informations implicites. Par exemple, quand je fais *2+2*, l’outil que j’utilise sait que *2* est un nombre et que comme il y a un *2*, le *+* ne va pas être sur les ordinaux mais sur les nombres. Lorsque l'on fait *n+1* avec *n* étant un entier, on sait que le *+* se fait entre entiers. Mais parfois on peut écrire *X+1* où *X* est un ensemble, en voulant dire qu'on construit l'ensemble étendant X avec un nouvel élément mais on peut aussi écrire *X+1* où *X* est un ensemble d'entiers en voulant dire qu'on dire qu'on va ajouter *1* à tous les éléments de l'ensemble.

L'élaboration est cette fonctionnalité des assistants à la preuve qui permet désambigüiser et de donner un sens précis à ce qui est écrit. Rocq, en 40 ans, a régulièrement intégré de nouvelles extensions de l'élaboration. Avec notre projet, nous sommes en train de mettre en place un langage de haut niveau par rapport à la logique formelle, que l'on voit en opposition comme un langage de bas niveau comparable à l'assembleur. Nous voulons créer pour la logique l'équivalent des langages fonctionnels de haut niveau, des langages qui sont proches de la manière dont raisonne les mathématiciens, en les accompagnant d'une chaîne d'interprétation, d'élaboration, et de compilation vers les langages formels bas niveau tels que ceux introduits historiquement par Gottlob Frege.

Dans la programmation, il y a des langages dédiés pour l'analyse, la probabilité, l'algèbre etc. qui s'écrivent dans une certaine langue naturelle dédiée. Une des questions du projet est justement de comprendre comment définir ces langues, comment les écrire puis comment les traduire. Nous souhaitons donc participer à cette chaîne de traduction.

Les LLM, dont on a le code, ne sont pas conçus pour raisonner mais pour recoller des bouts de phrases et construire un sens pour utiliser des éléments statistiques (essayer de comprendre quel est le prochain mot ou celui à l'intérieur d'une phrase). La construction d'un sens commun, lorsque deux personnes échangent par exemple, ne repose que sur notre construction personnelle. De même, lorsqu'on lit un texte mathématique, nous sommes en construction, à chaque étape, de façon interne, puisque nous essayons de comprendre le sens du texte. Lorsqu’on travaille au tableau, de la même manière, on fabrique du sens ensemble. L'expérience mathématique s'inscrit à l'intérieure de l'expérience humaine rationnelle.

Ce que considère Paul-André, c'est que la complexité du machine learning est justement d’arriver à transporter ce sens implicite, c'est à dire que les structures du machine learning soient capables de faire une représentation mentale, ce que la langue syntaxique n'est pas capable de faire puisqu'elle est d'une certaine manière séquentielle et non géométrique. Hugo considère justement que cette distance entre la langue séquentielle et la langue spatiale associée à la représentation mentale peut elle-même être étudiée d'un point de vue formel, linguistique et informatique.

Se pose donc la question des grandes dimensions. Comme dirait Stéphane Mallat, il y a beaucoup d'éléments, de features, la dimension des nombres étant gigantesque. La force du discours symbolique est qu'il y a une réduction qui contient pourtant les éléments, les indices qui permettront de reconstruire le sens. C'est comme ça que les maths se distribuent et que l'on peut les expliquer. Ces articulations peuvent être difficiles si on ne prend pas en compte la structure de la langue.

Aujourd'hui, les enjeux se portent sur les outils d'intelligence artificielle largement utilisés, comme Chat GPT et AlphaProof. De notre point de vue, il ne s'agit pas juste qu'un ordinateur comprenne des maths et arrive à les fabriquer mais plutôt de comprendre son mécanisme, presque de manière anthropologique.

Les LLM restent intrinsèquement liés aux Hommes, qui fabriquent des objets qui leurs ressemblent, qui font du sens. Et avant même la question de ces objets, il y a la question de comment le sens s'échange et comment les représentations mentales et les expressions physiques se comprennent. Les mathématiques, d’une certaine manière, sont incarnées, on va même jusqu’à parler d'expérience mathématique. Le texte mathématique, lui, produit et donne une information concise, mais ce sont des intuitions qui ressortent de manière intertextuelle. Quelque part, les LLM questionnent cela, pour comprendre comment un texte peut en appeler un autre. Les LLM n'ont pas accès au visage, à l'esprit mais seulement à du texte en très grande quantité, et de manière étonnante, un sens semble émerger (il n'est pas toujours très juste mais ça reste non pas moins étonnant).

Le projet ANR CoREACT de Nicolas Behr a certains liens avec cette ERC, puisqu'il travaille sur le raisonnement diagrammatique en mathématiques. C'est une manière de communiquer avec la machine qui passe par une représentation géométrique, mais qui a une structure formelle que nous essayons de caractériser. De même, Julien Narboux, travaille lui aussi sur des outils d'interaction graphique pour Rocq. Il manipule la langue formelle à partir d'un outil qui permet de dessiner des points, des lignes et des droites.

Pour ce qui est des voyages intercontinentaux, nous souhaitons adopter une règle de séjour long et de favoriser des évènements sur trois mois, pour fonctionner en trimestres. Ce procédé nous donne un cadre pour des échanges concentrés sur une période donnée. Le principe de trimestres thématiques se fait dans de nombreux établissements, comme à l’IHP par exemple. Nous voudrions nourrir cette façon de travailler avec notre projet.

Il y a 10 ans, nous avions organisé un trimestre à l'IHP avec Pierre-Louis Curien ; nous aimerions le refaire. Ce trimestre avait marqué les participant-e-s, qui s'en souviennent encore et comme nous en avons parlé plus haut, il est important pour nous de construire du sens dans notre métier. Selon nous, le modèle actuel des chercheurs de travailler sous contrat avec une durée relativement courte sous projet est un obstacle à la recherche dans le temps long.

Grâce à ERC, nous avons 6 ans et nous voulons donner du temps à la communauté européenne et internationale qui travaillent sur ces sujets, leur donner un lieu (Paris) où les chercheurs peuvent se rencontrer. Le projet ERC donne un cadre et aide à une réflexion qui dépasse largement le projet, qui ressemble à un forum et un lieu d'échange en dehors de toute compétition, pour comprendre ensemble comment faire avancer la connaissance et les usages.