Les LLM démontrent des théorèmes, mais ne découvrent pas de mathématiques : des chercheurs décrivent la prochaine étape

Un groupe de chercheurs a publié début juillet 2026 sur arXiv un article de position qui récapitule les avancées des prouveurs de théorèmes à base de LLM et met en évidence leur limite fondamentale : les systèmes actuels démontrent des théorèmes, mais ne savent pas découvrir de mathématiques. L'article propose aussi une feuille de route stratégique vers de véritables agents de recherche.

Ce que savent faire les systèmes AI4Math aujourd'hui

En quelques années, les systèmes LLM dédiés aux mathématiques formelles ont fait des progrès tangibles. En travaillant avec des langages de preuve interactive de théorèmes (ITP), surtout Lean 4, Isabelle et Coq, ils ont appris à générer des preuves formelles pour des problèmes bien posés. Ces langages permettent d'écrire les preuves de façon qu'un ordinateur vérifie mécaniquement chaque étape, ce qui rend le résultat bien plus fiable que les preuves manuscrites traditionnelles.

Les auteurs regroupent les avancées du domaine en trois axes :

• Jeux de données : des corpus de problèmes formalisés, du niveau scolaire au niveau universitaire, ont été constitués et permettent d'entraîner les modèles sur des exemples de preuves correctes
• Autoformalisation : les modèles traduisent mieux les énoncés rédigés en langage naturel vers la syntaxe formelle stricte des ITP
• Synthèse de preuves : les systèmes trouvent de plus en plus sûrement des preuves étape par étape lorsque l'énoncé de départ est clair

Tous ces progrès ont un point commun : ils ne fonctionnent que sur des problèmes bien définis et formulés à l'avance. Le modèle sait précisément ce qu'il doit démontrer et cherche le chemin vers cet objectif.

Pourquoi ce n'est pas encore de la science

La vraie recherche mathématique diffère radicalement de la résolution d'un recueil d'exercices. Elle exige de savoir formuler des conjectures, repérer des liens inattendus entre domaines différents et s'attaquer à des problèmes ouverts, souvent vieux de plusieurs années, mal définis et mobilisant plusieurs niveaux d'abstraction. C'est là que les systèmes LLM actuels montrent des limites systématiques.

Les auteurs relèvent cinq problèmes clés :

• Données : les jeux de données ne contiennent pas d'exemples de la façon dont naissent de nouveaux théorèmes, seulement la résolution de problèmes déjà posés
• Structure : les mathématiques reposent sur des hiérarchies complexes de concepts et sur des dépendances implicites entre branches, que les LLM assimilent mal
• Recherche : les modèles savent répondre à des questions, mais pas en formuler de nouvelles, ce qui est pourtant le fondement de la science
• Outils : il n'y a pas d'intégration avec les systèmes de calcul formel ni avec des bases de données mathématiques spécialisées
• Collaboration : les modèles ne peuvent pas être de véritables coauteurs, car ils ne comprennent pas le contexte informel que les scientifiques se transmettent

«

La prochaine percée en AI4Math exige un virage décisif : passer de solveurs de problèmes prédéfinis à des agents de recherche capables de travailler à la frontière des mathématiques » — la thèse centrale de l'article.

À quoi devrait ressembler le prochain système

La feuille de route stratégique décrite dans l'article prévoit la transition vers des agents mathématiques de recherche : des systèmes capables de formuler eux-mêmes des conjectures, de planifier un programme de recherche, d'échanger avec les scientifiques sous forme de dialogue et d'affiner de façon itérative l'énoncé du problème.

Cela suppose de faire progresser en parallèle plusieurs chantiers : de nouveaux jeux de données avec des exemples de découvertes réelles, des méthodes pour traiter les structures relationnelles des mathématiques, des écosystèmes d'outils plus matures et des modèles de collaboration homme-machine radicalement différents. Aucun de ces éléments n'existe encore sous la forme voulue, ce qui rend la tâche immense, mais clairement formulée.

Ce que cela signifie

L'article signale un changement important dans l'horizon des tâches de l'AI4Math : des systèmes qui vérifient des preuves vers des systèmes capables de participer à la découverte de nouvelles mathématiques. Cette transition demande une architecture radicalement différente d'une simple mise à l'échelle des approches existantes. Si la feuille de route proposée est mise en œuvre, les mathématiques pourraient devenir l'un des premiers domaines où l'IA joue le rôle de véritable partenaire de recherche du scientifique.