MALINCA : le projet qui ambitionne de réduire le fossé linguistique entre les mathématiciens et les machines

Nous aimons présenter notre projet en disant qu'il vise à combler le fossé linguistique existant entre le mathématicien et la machine. Quand on parle ici de machine, on pense plus particulièrement aux assistants à la démonstration, tels que Coq, qui sont des programmes permettant de développer des mathématiques dont la correction est assurée par ordinateur. Au cours de ces dernières années, ces programmes ont fait preuve d'une aptitude étonnante à s'attaquer à la formalisation complète et à la certification de résultats mathématiques conséquents et complexes (théorème de Feit-Thompson, conjecture de Kepler, défi du tenseur liquide de Scholze).

Ce succès nous fait penser qu'il est temps de doter les assistants à la démonstration de capacités leur permettant d'appréhender les mathématiques de la manière flexible et semi-formelle à laquelle recourent les mathématiciens dans la pratique quotidienne de leur travail.  En d'autres termes, nous voulons que la machine puisse analyser, comprendre et exploiter des textes mathématiques rédigés dans ce fragment particulier de la langue qu'utilisent les mathématiciens pour communiquer entre eux et publier leur résultats (fragment qui, bien que rigoureux, reste informel et présente la caractéristique de mêler langue naturelle et notations mathématiques).

S'il s'agissait de résumer notre projet sous la forme d'un slogan, nous dirions que le code ultime permettant d'interagir avec les assistants à la démonstration doit être la langue naturelle. Atteindre un tel but nécessite des recherches tant appliquées que fondamentales, en mathématiques, en informatique, en logique et en linguistique.

Notre projet ne nécessite pas de grands investissements en matériel. Il s'agit avant tout d'une aventure scientifique et humaine.  Nous entendons rassembler autour de notre objectif une équipe de chercheurs. En plus des quatre « principal investigators », notre projet inclut trois membres associés : David Alfaya de l'Université Pontificale de Comillas à Madrid, mathématicien spécialiste de l'apprentissage machine, Benoît Crabbé du Laboratoire de Linguistique Formelle de l'Université Paris Cité, spécialiste de traitement automatique des langues, et Daniela Petrișan de l'Institut de Recherche en Informatique Fondamentale de l'Université Paris Cité, spécialiste des sémantiques probabilistes.

Nous avons également prévu de financer douze thèses de doctorat, vingt-quatre années de séjours postdoctoraux, et le recrutement de deux ingénieurs. Nous prévoyons aussi de fédérer une communauté scientifique autour de notre thème de recherche par l'organisation de conférences, y compris des conférences thématiques résidentielles dans l'esprit des trimestres thématiques de l'Institut Henri Poincaré.

À l'origine du projet, il y a une réflexion au sein de l'équipe-projet Inria Pi.r2 sur la formalisation des mathématiques, le développement des assistants à la démonstration, les fondements logiques des mathématiques. Très vite, cette discussion a débouché sur une question centrale d'apparence élémentaire : « Qu'est-ce qu'une démonstration mathématique ? ».

Il y a plusieurs réponses possibles à cette question. On pourrait soutenir la thèse radicalement formelle selon laquelle une démonstration est un terme d'un certain type au sein du calcul des constructions (la théorie des types à la base d'assistants à la démonstration tels que Coq et Lean). On peut adopter un point de vue plus sémantique consistant à dire qu'une démonstration est un objet mathématique permettant d'interpréter un tel terme. On peut également apporter la réponse pragmatique qu'une démonstration est un texte réputé comme tel apparaissant dans un livre de mathématiques ou dans un article scientifique. On peut même défendre le point de vue psychologique et sociétal qui définirait une démonstration comme étant une représentation mentale communicable, reconnue et validée comme telle par la communauté des mathématiciens. On s'aperçoit alors que toutes ces réponses ne sont que les facettes d'une même réalité et que la question fondamentale est celle de la nature profonde d'une démonstration. Cette réflexion déboucha tout naturellement sur l'idée de combiner des expertises en informatique théorique, en théorie de la démonstration, en développement logiciel, en linguistique formelle, et en mathématiques.

Au fil des discussions, le projet s'est étoffé sur le plan applicatif, en intégrant l'idée d'utiliser des techniques d'apprentissage machine et de traitement automatique de la langue pour développer une nouvelle génération d'assistants à la démonstration qui seraient pilotés par la langue naturelle tout en restant ancrés dans des fondations mathématiques solides.

À moyen terme, notre projet  devrait déboucher sur des applications à l'enseignement.  Il devrait aussi offrir aux chercheurs une plus grande facilité dans la publication de résultats scientifiques dont la correction mathématique serait formellement certifiée.  À plus long terme, les suites de notre projet pourraient permettre à tout un chacun d'accéder au domaine des « mathématiques assistées par ordinateur ».

Il y a encore une quarantaine d'année, lorsque l'on entreprenait des études d'ingénieur, de technicien, de designer ou d'architecte, on passait une grande partie de son temps à ce qu'il était convenu d'appeler le dessin technique.  Depuis, la conception assistée par ordinateur a quasiment relégué le papier calque, l'encre de chine, les plumes et les tables de dessin au rang d'antiquités.  L'objectif que nous poursuivons, une fois atteint, pourrait donner lieu à une révolution similaire dans la pratique des mathématiques.