Le 1er août 2026, le site officiel d’OpenAI a publié une annonce sobre, sans vidéo de démonstration ni visuels spectaculaires : une version interne d’Astra — leur modèle phare de nouvelle génération — a résolu d’un coup dix problèmes ouverts en mathématiques et informatique théorique. Certains de ces problèmes résistaient depuis des décennies aux efforts de générations de mathématiciens et de lauréats du prix Turing. En l’espace de 24 heures, plus de 600 commentaires ont été publiés sur Hacker News. Mais le chiffre le plus frappant reste le coût : OpenAI a indiqué que les frais d’inférence combinés pour l’ensemble des dix problèmes s’élevaient à environ 2 000 dollars.
Que représentent 2 000 dollars dans ce contexte ? C’est inférieur à l’allocation mensuelle d’un doctorant. Cela marque un changement de paradigme : le coût des essais et erreurs dans la recherche mathématique passe des « années-hommes » aux « dollars ». Il convient toutefois de préciser que ce montant correspond uniquement aux coûts d’inférence calculés aux tarifs publics de l’API. Il n’inclut pas les investissements colossaux consacrés à l’entraînement du modèle, et personne ne connaît le nombre de tentatives infructueuses avant d’atteindre ce résultat.
Figure : Image de couverture publiée sur le site d’OpenAI pour les dix avancées mathématiques. Source : openai.com
Pourquoi ces problèmes mathématiques sont si difficiles
Il suffit de mesurer la portée de ces questions : les dix sujets touchent à la géométrie en grande dimension, à la théorie des codes, à la théorie des groupes, à l’informatique quantique, à la cryptographie et à la théorie des graphes. Citons trois exemples marquants :
« Existe-t-il des groupes non sofiques ? » — question centrale en théorie des groupes dont l’existence était largement conjecturée, mais que personne n’avait réussi à construire en plus de vingt ans. La difficulté d’approximation du « Problème du vecteur le plus court » (SVP) — étudié par les cryptographes depuis trois ou quatre décennies car il conditionne les standards de chiffrement post-quantique. La borne inférieure des « Nombres de Ramsey multicolores », issue du problème n° 183 de la liste du célèbre mathématicien Paul Erdős.
Pourquoi ces problèmes sont-ils si complexes ? Une démonstration mathématique ressemble à la recherche d’une sortie dans un labyrinthe : chaque étape exige une justification logique irréfutable ; une seule erreur invalide l’ensemble du cheminement. Contrairement aux examens classiques, les problèmes ouverts ne disposent d’aucun corrigé — personne ne sait où se trouve la sortie, ni même si elle existe. Les chercheurs humains s’appuient sur l’intuition, l’expérience et la chance, ne pouvant explorer qu’une seule voie à la fois.
Une autre difficulté réside dans le blocage sur la « direction initiale ». Si le point de départ de l’argumentation est erroné, la technicité ultérieure ne sera d’aucun secours. Nul ne peut chiffrer le nombre de fausses pistes écartées au fil des décennies, mais chacune d’elles représente des années-hommes de travail.
Comment l’IA y est parvenue
La méthode d’OpenAI se résume en une phrase : laisser le modèle générer des milliers de « brouillons de preuves », puis les faire vérifier systématiquement par une machine.
L’outil central de ce processus s’appelle Lean. Lean est un assistant de preuve formelle qui agit comme un examinateur impartial : lorsque la preuve lui est soumise dans un format structuré, il vérifie la logique ligne par ligne. Ce qui est valide est accepté, ce qui est erroné est rejeté sans concession. Lors de l’entraînement, les étapes de raisonnement validées par Lean reçoivent des récompenses, enseignant ainsi au modèle à « rédiger des arguments vérifiables par construction ». La progression fulgurante des capacités mathématiques de l’IA ces deux dernières années repose largement sur ce correcteur automatique. Les mathématiques constituent l’un des rares domaines où la validité d’une démarche peut être évaluée de façon totalement objective.
Imaginez 100 000 avatars s’élançant simultanément dans un labyrinthe : la plupart se heurtent à des murets, tandis qu’une poignée parvient à la sortie. L’examinateur ne retient que les parcours réussis. Là où un humain explore un chemin à la fois, l’IA peut en tester 10 000 en parallèle, marquant un changement d’échelle majeur.
Dans le cas présent, la version interne d’Astra a généré un vaste ensemble de propositions de preuves, Lean a sélectionné les démonstrations rigoureuses, puis des chercheurs humains ont mis en forme les arguments sous forme d’articles avant que le modèle ne formalise à nouveau chaque étape pour une vérification machine. OpenAI a également publié le journal de raisonnement du modèle. Les dix problèmes ont été résolus pour un total d’environ 2 000 dollars de tokens.
Pourquoi cela intéresse tout le monde
Premièrement, l’IA a livré « des réponses inédites jamais rédigées par des humains ». Selon OpenAI, les résultats fondamentaux liés à ces problèmes n’avaient connu aucun progrès significatif depuis au moins une décennie. Auparavant, les démonstrations de l’IA en mathématiques consistaient à résoudre des problèmes de compétition ou à reproduire des théorèmes connus ; il s’agit cette fois de véritables questions ouvertes.
Deuxièmement, les mathématiques se situent en amont de la technologie. Le problème du vecteur le plus court concerne directement la cryptographie post-quantique ; l’empilement de sphères et la théorie des codes régissent les télécommunications et le stockage de données. À chaque fois que le socle mathématique progresse, les technologies appliquées finissent par suivre.
Troisièmement, la courbe des coûts s’est inversée. Le mathématicien Terence Tao a théorisé cette année la « Big Math » : les humains apportent la vision créative tandis que l’IA prend en charge le travail lourd d’exploration. Un coût de 2 000 dollars signifie que l’exploration massive par essais et erreurs, autrefois réservée aux équipes de recherche de premier plan, devient accessible aux chercheurs individuelle. Après l’invalidation de la conjecture des distances unitaires d’Erdős par OpenAI en mai 2026 grâce à l’IA, au moins cinq travaux humains ont prolongé cette piste — preuve que les productions de l’IA deviennent le point de départ de la recherche humaine.
Pour le grand public, le signal est clair : la capacité de l’IA à produire de « nouveaux théorèmes inédits » montre qu’elle s’éloigne du simple rôle de « perroquet stochastique ». Cette faculté ne restera pas cantonnée aux mathématiques pures et finira par irriguer l’ingénierie logicielle et matérielle, pour s’incarner dans les objets de notre quotidien.
Optimistes vs sceptiques : qui a raison ?
Les échanges sur Hacker News ont fait apparaître deux visions opposées.
| Position | Arguments clés |
|---|---|
| Optimistes | Les résultats sont authentiques et entièrement vérifiables ; la formalisation avec Lean réduit quasiment à zéro le risque d’erreur ou d’hallucination. Si un étudiant résolvait ne serait-ce que quelques-uns de ces problèmes, il serait considéré comme un candidat à la médaille Fields. C’est l’équivalent mathématique de la victoire de Deep Blue contre Kasparov en 1997. |
| Sceptiques | Il peut s’agir d’une approche par force brute (« espace de recherche massif + vérification automatique ») sans apport de concepts réellement nouveaux. OpenAI n’a pas rendu publics les prompts ni le taux d’échec. La progression suit peut-être une courbe en S plutôt qu’une exponentielle, s’apparentant plus à une ascension en montagne qu’à un vol en fusée. Les annonces d’entreprises comportent une part de marketing. En 1976, la vérification du théorème des quatre couleurs par ordinateur avait suscité le scepticisme sans dénaturer la discipline. |
Les deux camps avancent des arguments solides. La critique la plus incisive des sceptiques provient d’un utilisateur de HN : Lean ne vérifie que des « propositions formellement correctes » ; s’assurer que la proposition répond précisément au problème posé reste de la responsabilité humaine. La machine contrôle le processus déductif, non la compréhension globale du sujet. La réplique des optimistes est directe : depuis la vérification par ordinateur du théorème des quatre couleurs, celui-ci demeure un théorème établi et nul ne l’a infirmé en cinquante ans.
Conclusion
La communauté des mathématiciens affiche des réactions contrastées : si certains évoquent dans de longs essais « une nuit noire pour les mathématiques », d’autres y voient le point de départ d’une démocratisation de la discipline. OpenAI a cité la Déclaration de Leyde, reconnaissant l’existence du débat et choisissant de publier les preuves, le code formalisé et les journaux de réflexion du modèle — une démarche de transparence peu fréquente chez les acteurs de l’IA.
Savoir si l’IA remplacera les mathématiciens n’est pas la question essentielle. Trois faits sont établis : dix problèmes ouverts ont été résolus et vérifiés par Lean, le coût d’inférence est de l’ordre de 2 000 dollars, et le débat ne fait que commencer. La position la plus équilibrée consiste à confier la validité des preuves aux machines et à l’évaluation par les pairs, tout en laissant au temps le soin de dire si l’IA « comprend réellement » les mathématiques.
Liens de référence :
- OpenAI: Ten advances in mathematics
- Discussion sur HN (item?id=49157930)
