Au cours du week-end, Neel Somani, ingénieur logiciel, ancien chercheur quantitatif et fondateur d’une startup, testait les compétences mathématiques du nouveau modèle d’OpenAI lorsqu’il a fait une découverte inattendue. Après avoir transmis le problème à ChatGPT et l’avoir laissé réfléchir pendant 15 minutes, il est revenu à une solution complète. Il a évalué la preuve et l’a formalisée avec un outil appelé Harmonic – mais tout a été vérifié.
« J’étais curieux d’établir une référence pour savoir à quel moment les LLM sont effectivement capables de résoudre des problèmes de mathématiques ouverts par rapport à ceux où ils ont du mal », a déclaré Somani. La surprise a été que, grâce au dernier modèle, la frontière a commencé à avancer un peu.
La chaîne de pensée de ChatGPT est encore plus impressionnante, évoquant des axiomes mathématiques comme la formule de Legendre, le postulat de Bertrand et le théorum de l’étoile de David. Finalement, le modèle a trouvé un article de Math Overflow de 2013, dans lequel le mathématicien de Harvard Noam Elkies avait donné une solution élégante à un problème similaire. Mais la preuve finale de ChatGPT différait du travail d’Elkies sur des points importants et donnait une solution plus complète à une version du problème posé par le légendaire mathématicien Paul Erdős, dont la vaste collection de problèmes non résolus est devenue un terrain d’essai pour l’IA.
Pour quiconque est sceptique quant à l’intelligence artificielle, c’est un résultat surprenant – et ce n’est pas le seul. Les outils d’IA sont devenus omniprésents en mathématiques, depuis les LLM orientés formalisation comme Aristote d’Harmonic jusqu’aux outils de revue de littérature comme la recherche approfondie d’OpenAI. Mais depuis la sortie de GPT 5.2 – que Somani décrit comme « anecdotiquement plus compétent en raisonnement mathématique que les itérations précédentes » – le grand nombre de problèmes résolus est devenu difficile à ignorer, soulevant de nouvelles questions sur la capacité des grands modèles de langage à repousser les frontières de la connaissance humaine.
Somani étudiait les problèmes d’Erdős, un ensemble de plus d’un millier de conjectures du mathématicien hongrois conservées en ligne. Ces problèmes sont devenus une cible tentante pour les mathématiques basées sur l’IA, variant considérablement en termes de matière et de difficulté. Le premier lot de solutions autonomes est venu en novembre d’un modèle alimenté par Gemini appelé AlphaEvolve – mais plus récemment, Somani et d’autres ont trouvé que GPT 5.2 était remarquablement adepte des mathématiques de haut niveau.
Depuis Noël, 15 problèmes sont passés de « ouvert » à « résolu » sur le site Web d’Erdős – et 11 des solutions ont spécifiquement crédité les modèles d’IA comme étant impliqués dans le processus.
Le vénéré mathématicien Terence Tao a un regard plus nuancé sur les progrès sur sa page GitHub, dénombrant huit problèmes différents dans lesquels les modèles d’IA ont réalisé des progrès autonomes significatifs sur un problème d’Erdős, avec six autres cas où des progrès ont été réalisés en localisant et en s’appuyant sur des recherches antérieures. Il y a encore beaucoup de chemin à parcourir avant que les systèmes d’IA soient capables de faire des calculs sans intervention humaine, mais il est clair que les grands modèles ont un rôle important à jouer.
Événement Techcrunch
San Francisco
|
13-15 octobre 2026
À propos de Mastodon, Tao a émis l’hypothèse que la nature évolutive des systèmes d’IA les rend « mieux adaptés pour être appliqués systématiquement à la « longue traîne » des problèmes obscurs d’Erdős, dont beaucoup ont en réalité des solutions simples.
« En tant que tel, bon nombre de ces problèmes d’Erdő plus faciles sont désormais plus susceptibles d’être résolus par des méthodes purement basées sur l’IA que par des moyens humains ou hybrides », a poursuivi Tao.
Une autre force motrice est l’évolution récente vers la formalisation, une tâche à forte intensité de main-d’œuvre qui rend le raisonnement mathématique plus facile à vérifier et à étendre. La formalisation ne nécessite pas l’utilisation de l’IA ni même d’ordinateurs, mais une nouvelle génération d’outils automatisés a rendu le processus beaucoup plus facile. L’« assistant de preuve » open source Lean, développé par Microsoft Research en 2013, est devenu largement utilisé dans le domaine comme moyen de formaliser la preuve – et des outils d’IA comme Aristote d’Harmonic promettent d’automatiser une grande partie du travail de formalisation.
Pour le fondateur d’Harmonic, Tudor Achim, l’avancée soudaine dans la résolution des problèmes d’Erdő est moins importante que le fait que les plus grands mathématiciens du monde commencent à prendre ces outils au sérieux. « Je me soucie davantage du fait que les professeurs de mathématiques et d’informatique utilisent (des outils d’IA) », a déclaré Achim. « Ces personnes ont une réputation à protéger, donc quand ils disent qu’ils utilisent Aristote ou qu’ils utilisent ChatGPT, c’est une preuve réelle. »
