====== 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 ======

[{{:portraits:dsc00063.jpg?200 |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 (ERC). 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.**"//

===== Bonjour Hugo et Paul-André, vous avez obtenu avec deux autres PI un financement pour un projet ERC (European Research Council Executive Agency) Synergie. Félicitations ! Pouvez-vous nous expliquer pourquoi vous y avez concouru ? =====

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 chercheur.euse.s 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 les couloirs 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 sa construction** 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 notre 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'[[https://www.inria.fr/en/picube|équipe Picube]]**. Nous avons aussi bénéficié des **ressources de l'[[https://u-paris.fr/|Université Paris Cité]]** à travers le projet Aprapram mené avec [[https://webusers.imj-prg.fr/~riccardo.brasca/|Riccardo Brasca]] et [[https://webusers.imj-prg.fr/~antoine.chambert-loir/index.xhtml|Antoine Chambert-Loir]] de l'[[https://www.imj-prg.fr/en/|IMJ-PRG]]. 

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

===== Pouvez-vous nous présenter votre projet d’ERC, Malinca ?=====

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

Pour ma part ([[https://pauillac.inria.fr/~herbelin/|Hugo]]), dans mon travail de recherche, je m'attache à **développer des systèmes formels, que des logiciels informatiques peuvent comprendre, et dans lesquels les textes mathématiques peuvent être traduits pour vérifier la correction des preuves.** 

De mon côté ([[https://www.irif.fr/~mellies/|Paul-André]]), je suis une **approche fondationnelle et synthétique**, travaillant à **dégager les briques de base de la programmation et du raisonnement mathématique**, au moyen d’outils provenant de la logique linéaire, de la sémantique des jeux, des catégories de petite dimension et de la théorie des nœuds.   

La première personne à qui nous avons pensé lorsque nous avons échangé est [[https://members.loria.fr/PDegroote/|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 [[https://rocq-prover.org/|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 possible théoriquement depuis la fin du XIXe siècle avec l'avènement de la logique formelle, et technologiquement avec l'arrivée de l'informatique, c'est que **pour vérifier la correction logique d'un texte mathématique, il faut d'abord le traduire dans cette langue qui est une langue formelle, celle 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 appelés **assistants à la preuve**, comme Rocq, [[https://en.wikipedia.org/wiki/Agda_(programming_language)|Agda]], ou encore [[https://en.wikipedia.org/wiki/Lean_(proof_assistant)|Lean]].  

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 ensuite imposée à nous est [[https://math.univ-cotedazur.fr/~carlos/|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, [[https://math.univ-cotedazur.fr/~ah/|André Hirschowitz]], sur la **formalisation et l'enseignement des mathématiques en utilisant 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. **Par défaut, dans ce domaine, la validation des articles repose sur la langue naturelle et 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 alors que les chercheur.euse.s sont poussé.e.s à produire de plus en plus de travaux ? 

Les rapporteurs passent moins de temps sur les articles. Nous avons lu une analyse (( Article de Alan L. Carey, Michael G. Cowling et Peter G. Taylor, traduit dans le journal de la Société Mathématique de France, [[https://smf.emath.fr/system/files/filepdf/gaz-115_compressed.pdf|page 79 de la gazette 115]], Janvier 2018)) qui 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 complexes, supposés corrects, qu'ils ne regardent et ne vérifient pas, puisqu'ils n'ont pas le temps de le faire. Même si valider les résultats des publications dans les moindres détails est un travail dantesque, il est néanmoins très important pour la communauté. 

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** dont la pratique 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ématicien.ne.s l’utilisent lorsqu'ils.elles é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 général 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**. 

Nous avons contacté Carlos Simpson un peu par "hasard" en tant qu'un des rares mathématiciens ayant étudié les questions de formalisation. En échangeant avec lui, nous avons découvert qu'il s'intéressait au //machine learning//, qui s'était donc 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 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. 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. 
===== Pouvez-vous préciser ce qu’est un langage naturel ? Pourquoi souhaitez-vous le voir utiliser par les assistants de 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 générale, à 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, aux nombreuses définitions. Pourtant, bien qu'il y en ait plusieurs, celles-ci sont équivalentes à un certain niveau d'abstraction et les discours que les mathématicien.ne.s tiennent au sujet des réels ne dépendent pas moralement de la définition. 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 pouvons faire des choses que nous ne pouvons pas réaliser 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ée 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 pourrions avoir l'impression que parce que la langue naturelle mathématique est de la langue naturelle, 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 dernier peut-être sophistiqué : par exemple, **la langue mathématique est aussi capable de s'auto-référencer avec des méthodes de preuves** tel que : « en prenant la preuve du paragraphe précédent, remplacez X par Y » et vous obtenez une nouvelle preuve pour prouver un autre théorème. Ce sont des choses que l'on s’autorise et nous espérons pouvoir les mécaniser concrètement et en faire une liste à peu près exhaustive. A partir de celle-ci, nous pourrons **construire une grammaire de la langue naturelle 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, c'est un nouvel exercice pour bien transmettre le sens poétique de la langue initiale. 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 bien 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 le fait 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 cette 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 n'y avait qu'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 exploitent les **LLM (Large Language Models) pour la recherche de preuve en les guidant avec les mots utilisés dans les textes mathématiques**. 

> 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 à **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 se concentre sur la structure des objets, en faisant abstraction de l'imaginaire, on s'aperçoit parfois qu'on parle en fait exactement de la même chose avec des noms différents. En particulier, on peut 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 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. 

Paul-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 toutes ces 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é //[[https://fr.wikipedia.org/wiki/Automath|Automath]]// mené par [[https://nl.wikipedia.org/wiki/Nicolaas_Govert_de_Bruijn|Nicolaas Govert de Bruijn]], qui a ensuite été suivi, entre autres, aux côtés de [[https://en.wikipedia.org/wiki/Mizar_system|Mizar]], [[https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)|Isabelle]], [[https://en.wikipedia.org/wiki/Nuprl|NuPrl]], ... par le système Rocq, développé initialement par [[https://fr.wikipedia.org/wiki/Thierry_Coquand|Thierry Coquand]] et [[https://pauillac.inria.fr/~huet/|Gérard Huet]], vite rejoints par [[https://www.lri.fr/~paulin/|Christine Paulin-Mohring]] puis par [[https://www.lix.polytechnique.fr/Labo/Benjamin.Werner/|Benjamin Werner]] et [[http://www.lsv.fr/~dowek/|Gilles Dowek]]... 

===== Pour analyser la langue naturelle, sur quels outils pensez-vous vous appuyer ? =====

**Les synergies entre linguistique et logique symbolique peuvent aujourd'hui être étudiées ensemble grâce aux outils qui viennent du TAL** (traitement automatique des langues - NLP en anglais). Et dans ce cadre-là, **la bourse Synergie prend tout son sens, parce nous allons pouvoir également discuter avec des linguistes de leurs intérêts et leurs pratiques**.

Ce projet ERC compte quatre chercheurs principaux mais d’autres chercheurs y participent également comme [[https://www.irif.fr/~petrisan/|Daniela Petrişan]] et [[https://www.linguist.univ-paris-diderot.fr/~bcrabbe/|Benoît Crabbé]] (linguiste) spécialiste des TAL. Tous les deux s’intéressent particulièrement aux traductions, et notamment pour Benoît, à la construction de codes ou de programmes Python à partir d'une description linguistique. C'est un renouveau pour les TAL, avec une **nouvelle génération d'outils comme les LLM**. Mettre en vis à vis ces outils venant 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. En complément de l'équipe initiale, [[https://www.iit.comillas.edu/people/dalfaya|David Alfaya]], jeune mathématicien madrilène brillant, s'intéresse lui aux questions de //machine learning//, à la fois de manière théorique et pratique. 

> L’exercice des mathématiques, avec ses questions fondationnelles inscrites dans la tradition de la logique symbolique, confronté à l'arrivée des outils issus du //machine learning//, invite à se questionner sur les **liens entre méthodes formelles et 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.** 
Certains s'inquiètent que les nouveaux outils apparus récemment soient utilisés sans qu'on comprenne leurs mécanismes profonds. D'un autre côté, l'IRIF est un exemple d’institut attaché à** comprendre les fondations des structures profondes de l'informatique**. C'est un travail à faire aujourd'hui pour le //machine learning// : 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. 
 
===== Vous dites vouloir « développer des technologies d'assistant de preuve […], comprenant un langage formel et une approche fondamentale de la signification mathématique ». Est-ce que cela veut dire que l’approche fondamentale n’a jamais été utilisée avant pour construire des assistants de preuves ? =====

Les assistants à la démonstration reposent sur un travail fondamental mais également sur un savoir-faire technologique et algorithmique, qui fait aussi partie des fondations. Un des aspects du projet est de se saisir de **certaines évolutions empiriques des assistants à la preuve** et de les faire rentrer dans un cadre conceptuel. Nous pensons par exemple ici à un ensemble de techniques développées au fil des années pour libérer l'utilisateur de détails formels fastidieux, ensemble de techniques regroupées sous le nom d'**élaboration** et qui inclut par exemple la résolution des notations, l'inférence d'information implicite, l'inclusion implicite de structures mathématiques. Nous voulons aussi intégrer des techniques de //parsing// à l'élaboration et 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 [[https://ocaml.org/|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, 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 va ajouter **1** à tous les éléments de l'ensemble. 

> L'élaboration est cette fonctionnalité des assistants à la preuve qui **permet de 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 raisonnent 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 [[https://fr.wikipedia.org/wiki/Gottlob_Frege|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 à partir d'éléments purement 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érieur 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 le mathématicien [[https://fr.wikipedia.org/wiki/St%C3%A9phane_Mallat|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 mathématiques 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 , qu'ils soient largement utilisés comme ChatGPT, ou spécialisés pour la preuve comme 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 [[https://anr.fr/Projet-ANR-22-CE48-0015|ANR CoREACT]] de [[https://nicolasbehr.com/|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, [[https://www.irif.fr/~narboux/|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.

===== Vous souhaitez inscrire votre projet dans un environnement responsable écologiquement. Comment allez-vous faire ? =====

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’[[https://www.ihp.fr/fr|Institut Henri Poincaré (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 [[https://www.irif.fr/~curien/|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 à cette ERC, nous avons six 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.**