Au MIT, l’IA relie des bases de données aux preuves mathématiques formelles

En mathématiques, une intuition, un calcul convaincant ou un résultat répertorié ne suffisent pas à établir une preuve. Il faut encore dérouler chaque étape logique dans un cadre rigoureux. C’est précisément l’écart que veulent réduire David Roe et Andrew Sutherland, chercheurs au département de mathématiques du MIT, avec un projet qui connecte deux mondes encore largement séparés : les grandes bases de données de résultats et les assistants de preuve formelle.

Présenté en septembre 2025, leur travail fait partie des premiers projets financés par les subventions AI for Math, proposées par Renaissance Philanthropy en partenariat avec XTX Markets. L’ambition est importante, mais elle ne consiste pas à annoncer une machine qui résoudrait seule les grands problèmes ouverts. Il s’agit plutôt de construire une infrastructure : un moyen pour les chercheurs et, à terme, pour des agents d’IA, de passer plus facilement d’une connaissance mathématique disponible à une piste de formalisation ou de démonstration vérifiable.

Une subvention pour mieux outiller la découverte mathématique

David Roe et Andrew Sutherland travaillent à l’interface de la théorie des nombres, des données mathématiques et de l’informatique formelle. Leur projet cible un obstacle très concret : les assistants de preuve sont techniquement sophistiqués, mais ils restent moins dotés en ressources que ne le laisserait penser leur potentiel scientifique.

Un assistant de preuve est un logiciel qui vérifie qu’une démonstration respecte les règles logiques définies dans son langage. Il ne se contente pas de donner une réponse plausible. Pour qu’un théorème soit accepté, toutes les étapes nécessaires doivent pouvoir être contrôlées par le système. Cette exigence apporte une grande rigueur, mais elle a un coût : traduire des mathématiques rédigées pour des humains dans un langage formel peut demander beaucoup de temps et d’expertise.

Selon Andrew Sutherland, l’essor des grands modèles de langage abaisse toutefois la barrière d’entrée de ces outils. Ces modèles peuvent notamment aider à naviguer dans de vastes corpus, à suggérer des étapes de travail ou à assister la rédaction de code formel. Ils ne remplacent pas la vérification logique : dans un système formel, c’est bien le vérificateur qui décide si une preuve est valide.

Le financement AI for Math doit ainsi permettre de développer des outils de démonstration automatisée plus accessibles et mieux reliés aux connaissances déjà accumulées par la communauté mathématique. Le projet du MIT s’inscrit aussi dans un ensemble plus large d’initiatives portées, entre autres, par des anciens élèves de l’établissement.

LMFDB et mathlib, deux ressources complémentaires

Le cœur du projet consiste à rapprocher la L-Functions and Modular Forms Database, plus connue sous l’acronyme LMFDB, et mathlib, la grande bibliothèque mathématique communautaire conçue pour l’assistant de preuve Lean 4.

Ces deux ressources n’ont pas le même rôle. La LMFDB est une base de données collaborative consacrée à la théorie des nombres moderne. Elle rassemble un volume considérable de connaissances spécialisées, sous la forme de données et d’énoncés concrets. Mathlib, de son côté, organise des définitions, lemmes et théorèmes sous une forme que Lean 4 peut vérifier.

La différence d’échelle éclaire l’intérêt du rapprochement. La LMFDB offre une cartographie extrêmement riche de résultats utiles aux spécialistes. Mathlib fournit, elle, un socle de connaissances fiables dans lequel un programme peut raisonner sans ambiguïté sur les objets déjà formalisés. Faire communiquer ces deux univers pourrait éviter aux chercheurs de partir d’un corpus beaucoup plus limité, celui des seuls résultats déjà formalisés.

Pourquoi la formalisation reste-t-elle difficile ?

La formalisation est l’un des grands goulots d’étranglement de la recherche assistée par ordinateur. Un article mathématique destiné à des spécialistes laisse souvent implicites des détails que les lecteurs compétents savent reconstruire. Un assistant de preuve ne peut pas combler ces ellipses de lui-même : les définitions doivent être précises, les hypothèses explicites et les lemmes intermédiaires disponibles dans le bon format.

Cette difficulté s’ajoute au nombre limité de connaissances déjà transcrites dans les bibliothèques formelles. Même lorsque le résultat à démontrer est bien connu, sa traduction peut être complexe si les notions nécessaires n’ont pas encore été définies dans l’environnement logiciel concerné. C’est pourquoi le coût humain de la formalisation de résultats avancés demeure élevé.

Le problème est particulièrement visible en théorie des nombres, un domaine où les objets étudiés peuvent être très structurés. Courbes elliptiques, corps de nombres, formes modulaires et fonctions L entretiennent des relations nombreuses. Pour un mathématicien, une base de données peut signaler une propriété intéressante ou suggérer une analogie. Pour un logiciel de preuve, il faut encore que les objets et les relations mobilisés soient décrits avec une précision formelle.

Dans la présentation du projet, les chercheurs évoquent notamment le dernier théorème de Fermat, démontré par Andrew Wiles. Cet exemple rappelle que les avancées majeures s’appuient souvent sur une connaissance très spécialisée, à la croisée de plusieurs domaines, ainsi que sur des calculs non triviaux. L’enjeu des outils numériques n’est donc pas de réduire les mathématiques à une recherche de mots-clés, mais de rendre plus maniable un espace de connaissances devenu immense.

Rendre les données accessibles sans les faire passer pour des preuves

Le projet de Roe et Sutherland prévoit de rendre les résultats de la LMFDB accessibles depuis mathlib sous la forme d’assertions qui ne sont pas encore prouvées formellement. Cette nuance est essentielle. Une information issue de la base peut guider une recherche, fournir une cible à étudier ou aider à sélectionner un cas intéressant. Elle ne doit pas être confondue avec un théorème dont la preuve a été vérifiée dans Lean 4.

L’idée est donc d’ouvrir une porte vers un corpus beaucoup plus vaste sans masquer la frontière entre les deux niveaux de certitude. Dans cette architecture, les données non formalisées peuvent nourrir l’exploration. La preuve formelle reste l’étape qui transforme une hypothèse ou un résultat connu en énoncé vérifié dans le système.

Cette séparation est importante autant pour les mathématiciens que pour les agents d’IA. Un agent qui n’accède qu’aux résultats déjà formalisés travaille dans un environnement très sûr, mais plus restreint. Un agent capable de consulter une base comme la LMFDB dispose de davantage de pistes, à condition que le statut de chaque information soit clairement indiqué.

David Roe estime que la possibilité d’explorer des théorèmes ou des preuves s’accroît de manière exponentielle lorsque les agents peuvent consulter un plus grand nombre de faits, au lieu de se limiter aux seuls éléments déjà formalisés. Il s’agit d’un potentiel de recherche, pas d’une garantie de découverte automatique. La qualité des données, la conception des outils et la capacité à produire ensuite des preuves valides restent déterminantes.

Des premières briques centrées sur la théorie des nombres

Les prochaines étapes annoncées sont concrètes. Les deux chercheurs veulent d’abord permettre d’effectuer des recherches dans la LMFDB depuis l’intérieur de mathlib. Cette fonctionnalité rendrait la consultation de la base plus naturelle pour une personne ou un outil qui travaille déjà dans l’environnement Lean 4.

Ils prévoient également de formaliser les définitions essentielles relatives à plusieurs objets présents dans la LMFDB : les courbes elliptiques, les corps de nombres et les formes modulaires. Ce choix répond à une logique de fondation. Avant de relier efficacement des résultats spécialisés, il faut disposer dans mathlib d’un vocabulaire formel suffisamment riche pour exprimer les objets concernés et leurs propriétés.

Une courbe elliptique est, malgré son nom, un objet algébrique central en théorie des nombres. Les formes modulaires sont des fonctions très structurées qui jouent un rôle profond dans ce domaine. Les corps de nombres généralisent les nombres rationnels dans un cadre qui permet d’étudier plus finement les équations et leurs solutions. Ces notions sont étroitement liées dans de nombreuses recherches modernes, ce qui en fait un terrain pertinent pour tester l’intégration envisagée.

Le projet doit être mené en lien étroit avec les communautés qui font vivre la LMFDB et mathlib. Cette dimension communautaire compte : une bibliothèque formelle et une base de données ne progressent pas seulement grâce à des algorithmes, mais aussi grâce à des conventions partagées, des relectures et des contributions durables. David Roe invite d’ailleurs les étudiants du MIT qui souhaitent participer à cette dynamique à se manifester.

L’IA comme partenaire de méthode, pas comme arbitre de vérité

L’expression « IA pour les mathématiques » peut recouvrir des réalités très différentes. Certains outils aident à rédiger du code, d’autres recherchent des motifs dans des données, d’autres encore tentent de proposer des preuves. Dans le cas du projet du MIT, la priorité est de créer un cadre où les connaissances existantes deviennent plus faciles à interroger et à raccorder à un langage de preuve formelle.

Cette approche répond à une limite bien connue des modèles de langage : ils peuvent produire des raisonnements qui semblent convaincants sans être exacts. Dans les mathématiques formelles, la vérification automatique offre une protection essentielle contre ce risque. Une proposition issue d’un humain ou d’une IA n’acquiert pas le statut de preuve avant d’avoir passé le contrôle du système.

Le rapprochement de la LMFDB et de mathlib cherche ainsi à tirer parti de deux forces distinctes. Les bases de données apportent l’ampleur et la richesse des connaissances accumulées. Les outils formels apportent la précision et la traçabilité des démonstrations. Les modèles d’IA peuvent servir d’interface ou d’assistance entre ces couches, mais l’objectif demeure une recherche mathématique plus rigoureuse autant que plus productive.

Ce qu’il faut surveiller

La réussite du projet ne se mesurera pas uniquement au nombre d’entrées reliées entre deux logiciels. Il faudra observer si les recherches dans la LMFDB depuis mathlib deviennent réellement utiles aux praticiens, si les définitions de base sont suffisamment réutilisables, et si la séparation entre assertions non formalisées et résultats vérifiés reste parfaitement lisible.

Un autre enjeu sera l’extension de la méthode. Roe et Sutherland envisagent un cadre capable de connecter, au-delà de la LMFDB, d’autres bases de données mathématiques à des systèmes de démonstration formelle. Si cette infrastructure s’avère robuste, elle pourrait aider les chercheurs à transformer plus vite des connaissances dispersées en objets formels réutilisables.

À court terme, le projet ne rendra pas inutile le travail des mathématiciens. Au contraire, il met en lumière sa valeur : choisir les bonnes conjectures, formuler les bonnes définitions, interpréter les résultats et construire les preuves. L’IA et les assistants de preuve peuvent élargir l’espace des pistes explorables. La découverte, elle, restera liée à la rigueur collective qui fait des mathématiques une science de la démonstration.