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

Un groupe de chercheurs a publié un article de positionnement sur arXiv au début de juillet 2026 qui a systématisé les réalisations des prouveurs de théorèmes basés sur les LLM et identifié leur limitation fondamentale : les systèmes actuels prouvent des théorèmes mais sont incapables de découvrir les mathématiques — et ont proposé une feuille de route stratégique pour la transition vers des agents de recherche à part entière.

Ce Que les Systèmes AI4Math Savent Faire Aujourd'hui

Au cours des dernières années, les systèmes LLM pour les mathématiques formelles ont réalisé des progrès tangibles. Travaillant avec des langages pour la preuve interactive de théorèmes (ITP) — principalement Lean 4, Isabelle et Coq — ils ont appris à générer des preuves formelles pour des problèmes bien définis. Ces langages permettent d'écrire les preuves de sorte qu'un ordinateur puisse vérifier mécaniquement chaque étape — ce qui rend le résultat fondamentalement plus fiable que les preuves manuscrites traditionnelles.

Les auteurs ont systématisé trois directions clés du développement du domaine :

• Ensembles de données — des corpus de problèmes formalisés se sont accumulés, du niveau du lycée au niveau universitaire, permettant d'entraîner des modèles sur des exemples de preuves correctes
• Autoformalisation — les modèles se sont améliorés dans la traduction des énoncés de problèmes écrits en langage naturel en syntaxe formelle stricte d'ITP
• Synthèse de preuves — les systèmes trouvent de plus en plus avec assurance des preuves étape par étape quand on leur donne une formulation initiale claire

Toutes ces réalisations partagent une caractéristique : elles ne fonctionnent que sur des problèmes bien définis et pré-formulés. Le modèle sait exactement ce qui doit être prouvé — et cherche le chemin vers cet objectif.

Pourquoi Ce N'est Pas Encore de la Science

La véritable science mathématique est fondamentalement différente de la résolution de problèmes. Elle nécessite la capacité à formuler des hypothèses, identifier des connexions inattendues entre différents domaines et attaquer des problèmes ouverts — souvent de longue date, mal formulés et nécessitant plusieurs niveaux d'abstraction. C'est précisément ici que les systèmes LLM actuels démontrent des limitations systémiques.

Les auteurs identifient cinq problèmes clés :

• Données : les ensembles de données ne contiennent pas d'exemples de la façon dont naissent les nouveaux théorèmes — seulement la solution de problèmes déjà posés
• Structure : les mathématiques reposent sur des hiérarchies complexes de concepts et des dépendances implicites entre branches, que les LLM assimilent mal
• Exploration : les modèles peuvent répondre aux questions mais ne peuvent pas en formuler de nouvelles — or c'est là le fondement de la science
• Outils : il n'y a pas d'intégration avec les systèmes d'algèbre informatique et les bases de données mathématiques spécialisées
• Collaboration : les modèles ne peuvent pas être de véritables collaborateurs — ils ne comprennent pas le contexte informel que les scientifiques se transmettent les uns aux autres

«

Le prochain progrès en AI4Math exige un virage décisif des solveurs de tâches prédéterminées aux agents de recherche capables de travailler à la frontière des mathématiques » — la thèse clé de l'article.

Ce Que le Prochain Système Devrait Être

La feuille de route stratégique décrite dans l'article envisage une transition vers des agents de recherche mathématique — des systèmes capables de formuler indépendamment des hypothèses, de planifier des programmes de recherche, d'interagir avec les scientifiques en mode dialogue et d'affiner itérativement les formulations des problèmes.

Cela nécessitera le développement simultané de plusieurs directions : de nouveaux ensembles de données avec des exemples de vraies découvertes, des méthodes pour travailler avec les structures relationnelles des mathématiques, des écosystèmes d'outils plus matures et des modèles fondamentalement différents de collaboration humain-machine. Aucun de ces composants n'existe encore sous la forme nécessaire — ce qui rend la tâche à grande échelle mais clairement formulée.

Ce Que Cela Signifie

L'article signale un changement important à l'horizon de l'AI4Math : des systèmes de vérification de preuves aux systèmes capables de participer à la découverte de nouvelles mathématiques. Cette transition nécessite une architecture fondamentalement différente de la simple mise à l'échelle des approches existantes. Si la feuille de route proposée est réalisée, les mathématiques pourraient devenir l'un des premiers domaines où l'IA devient un véritable partenaire de recherche pour le scientifique.