Il y a cinq ans, voir un modèle de langage résoudre un problème mathématique en plusieurs étapes relevait presque de la curiosité. Aujourd’hui, la question n’est plus seulement de savoir s’il peut résoudre des exercices, mais ce qui arrive lorsqu’il commence aussi à produire des résultats de recherche.
Ce changement dépasse largement les classements de benchmarks. Pendant des siècles, obtenir une nouvelle démonstration a été une activité rare : elle pouvait demander des mois, des décennies ou toute une carrière. Publications, réputation, formation et une grande partie de la culture mathématique se sont construites autour de cette difficulté.
Si la production de preuves commence à passer à l’échelle informatique, la rareté ne disparaît pas. Elle se déplace.
Des exercices aux problèmes ouverts
La progression récente explique pourquoi le débat a changé si vite.
En 2021, OpenAI a publié GSM8K parce que les grands modèles échouaient encore systématiquement sur des problèmes élémentaires exigeant plusieurs étapes. Un an plus tard, Minerva de Google améliorait nettement les résultats sur des questions techniques allant du lycée à l’université et aux sciences quantitatives.
En 2023, FunSearch a associé un modèle générant des programmes à un évaluateur automatique. Il a trouvé de nouvelles constructions pour le cap set problem et de meilleures heuristiques de bin packing. Le saut conceptuel était important : les candidats pouvaient être testés et conservés lorsqu’ils amélioraient l’état de l’art.
En 2024, AlphaGeometry s’est approché du niveau moyen d’un médaillé d’or humain sur un ensemble de problèmes historiques de géométrie olympique. AlphaProof et AlphaGeometry 2 ont ensuite résolu quatre des six problèmes de l’Olympiade internationale de mathématiques : 28 points sur 42, niveau médaille d’argent.
En juillet 2025, une version avancée de Gemini Deep Think a atteint le niveau or : cinq problèmes, 35 points et des démonstrations en langage naturel dans la limite de 4,5 heures. La barrière symbolique des compétitions était tombée. Restait une distinction confortable : une olympiade n’est pas de la recherche.
En 2026, la nature des preuves change
First Proof a testé directement cette frontière. Le projet a réuni dix problèmes issus de travaux de recherche réels, dont les solutions étaient connues de leurs auteurs mais jamais publiées. Quatre systèmes ont travaillé dans des conditions contrôlées et 30 spécialistes ont évalué les réponses.
Pour sept problèmes sur dix, au moins un système a produit une solution jugée pratiquement irréprochable ou ne nécessitant que des corrections mineures. Le rapport documente aussi les faiblesses : les systèmes détaillaient souvent les parties routinières tout en survolant l’étape la plus difficile, et certaines citations ne soutenaient pas les affirmations avancées.
C’est plus instructif que de dire que « l’IA fait des mathématiques ». Le résultat montre une capacité réelle sur un petit échantillon, ainsi que les défauts qui apparaissent lorsque des textes plausibles sont soumis à une expertise rigoureuse.
En mai, OpenAI a publié un contre-exemple généré par un modèle interne qui réfutait une conjecture d’Erdős sur les distances unitaires dans le plan. Des mathématiciens externes ont vérifié la preuve et rédigé un article complémentaire pour l’expliquer et la contextualiser.
En août, OpenAI a présenté dix résultats de son système interne Astra en géométrie, théorie des codes et des groupes, complexité, cryptographie et combinatoire. L’entreprise affirme que le système a généré les arguments, que des humains ont préparé les manuscrits avec le modèle, puis que celui-ci a formalisé chaque argument dans Lean. Les résultats sont publics et vérifiables, mais leur portée à long terme doit être établie par la communauté mathématique, pas par l’annonce d’une entreprise.
Quelques jours plus tard, Anthropic a annoncé une autre avancée frappante. Une version expérimentale de Claude a tenté d’attaquer l’hypothèse de Riemann. Elle ne l’a pas résolue. Au cours de cette tentative, elle a produit un argument faisant passer de 41,6 % à 67,2 % une borne inférieure liée à la proportion de zéros de la fonction zêta situés sur la droite critique.
Cela ne signifie pas que l’hypothèse est « résolue à 67 % ». Anthropic précise que cette technique ne devrait pas mener à sa démonstration. Deux mathématiciens de l’entreprise ont validé le travail, des spécialistes externes l’ont examiné et une formalisation Lean existe. C’est un progrès sur une question connexe, pas une fraction de la conjecture principale.
Vérifier une preuve n’est pas la comprendre
Les mathématiques ont un avantage singulier sur les autres sciences. Une molécule proposée par un modèle a encore besoin d’un laboratoire. Une démonstration peut être traduite en objet formel et vérifiée pas à pas par un petit noyau logiciel. Lean n’a pas besoin de croire à la réputation d’une entreprise ou à l’intuition d’un auteur.
Mais la vérification formelle répond à une question limitée : la conclusion découle-t-elle des axiomes et définitions encodés par des inférences valides ? Elle ne dit pas si la formalisation correspond exactement à l’énoncé visé, si la preuve explique quelque chose ou si le résultat mérite notre attention.
Une preuve de cent mille lignes peut être correcte et rester inutilisable pour une communauté qui n’en comprend pas l’idée centrale. La transformer en prose fluide ne suffit pas non plus : une explication trop polie peut masquer les choix, les impasses et les connexions par lesquels on apprend réellement un argument.
De la rareté à l’indigestion des preuves
Terence Tao décrit le risque comme un passage de la rareté à l’abondance des démonstrations. Si l’on suppose que l’IA accomplira une part significative des tâches de recherche, une chaîne de goulots d’étranglement apparaît :
- générer une preuve candidate ;
- vérifier sa correction ;
- l’expliquer pour que d’autres la comprennent ;
- permettre à la communauté de l’évaluer et de l’utiliser ;
- l’intégrer aux théories, aux cours et aux manuels.
Automatiser la première étape n’automatise pas les autres. Cela peut au contraire les saturer. Les preuves peuvent s’accumuler plus vite que nous ne pouvons les évaluer, les lire et les transformer en savoir partagé.
Le problème précède l’IA. La spécialisation, la longueur de certains travaux et la pression sur l’évaluation scientifique avaient déjà produit une littérature difficile à digérer. La génération massive peut multiplier ce décalage.
La valeur n’a peut-être jamais résidé uniquement dans le théorème
Résoudre des problèmes n’est qu’une partie de l’activité mathématique. Choisir de bonnes questions, construire des définitions, trouver des connexions, former le jugement, enseigner et maintenir une communauté sont tout aussi importants.
Historiquement, ces activités étaient corrélées. Produire une démonstration difficile exigeait généralement une compréhension profonde ; le processus faisait émerger techniques, intuitions et nouvelles questions. « Démontrer un résultat » pouvait donc servir d’indicateur approximatif de nombreuses autres contributions.
L’IA peut rompre cette corrélation. Si générer une preuve prend quelques minutes mais comprendre son mécanisme plusieurs mois, le résultat ne suffit plus à mesurer la valeur du travail.
Des questions plus difficiles apparaissent alors :
- Qui mérite le crédit lorsque des acteurs différents génèrent, sélectionnent, vérifient et expliquent une preuve ?
- Comment former des mathématiciens si l’on automatise précisément les étapes difficiles par lesquelles ils apprennent ?
- Comment prioriser une littérature qui croît plus vite que notre capacité de lecture ?
- Une théorie peut-elle être formellement correcte sans qu’aucune personne ne la comprenne dans son ensemble ?
- Quelles activités doivent rester humaines, même lorsqu’elles peuvent être automatisées ?
La réponse n’est ni de rejeter toute automatisation ni d’accepter tout ce qui passe un vérificateur. Il faut concevoir des processus où génération, validation, attribution et explication sont séparées et visibles.
L’IA ne rend pas les mathématiques moins intéressantes. Elle empêche de continuer à confondre production de preuves et construction de compréhension. Si démontrer cesse d’être la partie difficile, nous découvrirons peut-être que la valeur résidait aussi dans le choix de ce qu’il faut démontrer, dans la raison pour laquelle cela compte et dans la manière de le rendre compréhensible aux autres.
Sources
- OpenAI : GSM8K
- Google Research : Minerva
- Google DeepMind : FunSearch
- Google DeepMind : AlphaProof et AlphaGeometry 2 à l’IMO 2024
- Google DeepMind : Gemini Deep Think à l’IMO 2025
- First Proof : rapport de la deuxième série
- OpenAI : contre-exemple à la conjecture des distances unitaires
- OpenAI : dix avancées en mathématiques et informatique théorique
- Anthropic : progrès lié à la fonction zêta de Riemann
- Terence Tao : Mathematics in the age of AI
