OpenAI vient-il de tuer les mathématiques traditionnelles ?

Réponse courte : non. Mais OpenAI vient peut-être de rendre obsolète une partie de leur économie traditionnelle. Quand un modèle peut produire en quelques semaines des centaines de manuscrits sur des problèmes de recherche, le résultat rare n’est plus forcément la preuve elle-même. Ce qui devient rare, c’est le temps humain nécessaire pour vérifier, comprendre, relier et transmettre cette preuve.

Le 6 octobre 2026, OpenAI a publié un dépôt contenant 722 manuscrits regroupés en 372 familles de résultats, issus pour l’essentiel d’un même modèle interne. Ce n’est pas une preuve isolée ni un nouveau record sur un benchmark : c’est une démonstration de production mathématique à grande échelle.

Cette annonce est majeure. Elle ne permet pourtant pas de conclure que 372 grandes conjectures ont été définitivement résolues, ni que les mathématiciens sont devenus inutiles.

Ce qu’OpenAI a réellement publié

Le dépôt couvre de nombreux domaines, de la théorie des nombres à la physique mathématique, en passant par la géométrie, l’analyse et l’informatique théorique. Une « famille » peut réunir un résultat principal, des conséquences, des preuves alternatives ou des textes complémentaires : 372 familles ne signifient donc pas 372 problèmes ouverts indépendants résolus.

OpenAI indique avoir soumis environ 4 000 problèmes à un modèle de frontière non encore publié. Chaque résultat retenu aurait consommé, en moyenne, l’équivalent de trois heures de raisonnement avec ChatGPT Pro. L’entreprise ne donne pas pour autant un taux de réussite simple : les résultats ont été regroupés, filtrés et sélectionnés selon leur niveau de portée. Diviser 372 par 4 000 ne mesurerait donc pas proprement les capacités du modèle.

L’échelle reste impressionnante. Jusqu’ici, les annonces d’IA en mathématiques se concentraient souvent sur un problème spectaculaire ou une dizaine d’avancées. Ici, le signal est différent : la génération de recherche pourrait devenir industrielle.

Une preuve publiée n’est pas encore un savoir partagé

Le dépôt réunit des travaux à des stades de vérification différents. OpenAI le reconnaît explicitement : tous les résultats ne disposent pas d’une formalisation en Lean, et certains textes non formalisés peuvent contenir des erreurs.

Lean est un assistant de preuve. Lorsqu’une démonstration y est correctement formalisée et acceptée par son noyau logique, on obtient une garantie très forte sur la proposition encodée. Mais cela ne répond pas automatiquement à toutes les questions importantes :

• la proposition formalisée correspond-elle exactement à celle annoncée en langage courant ?
• les définitions et hypothèses traduisent-elles bien le problème original ?
• le résultat est-il réellement nouveau et correctement attribué ?
• la preuve est-elle intéressante, éclairante ou réutilisable ?
• la communauté en comprend-elle les idées ?

Une vérification formelle n’est donc ni un simple gadget, ni un certificat universel. Elle contrôle une démonstration précise ; elle ne juge pas à elle seule sa portée scientifique.

Un audit humain indépendant des dix avancées publiées par OpenAI en août 2026 illustre bien cette distinction. Les auteurs n’y ont trouvé aucun défaut mathématique substantiel confirmé dans les résultats principaux examinés, mais ils signalent une profondeur de relecture inégale et, pour l’un des chapitres, des passages analytiques encore trop condensés pour parler de vérification complète. Même avec des certificats Lean, la correspondance entre énoncé formel, manuscrit et promesse publique reste un travail humain.

Le vrai bouleversement : 722 textes arrivent d’un coup

Les mathématiques traditionnelles reposent sur une chaîne relativement lente : poser une bonne question, chercher, échouer, discuter, rédiger, soumettre, relire, corriger, expliquer et laisser d’autres chercheurs réutiliser le résultat.

L’IA compresse brutalement la phase de production. Elle ne compresse pas nécessairement au même rythme l’assimilation collective. Aucun département, comité éditorial ou groupe de spécialistes ne peut lire sérieusement 722 manuscrits en quelques jours.

Le goulot d’étranglement se déplace donc :

• de la recherche d’une preuve vers le choix des résultats dignes d’attention ;
• de l’écriture vers la vérification et l’exposition ;
• de la rareté des réponses vers la qualité des questions ;
• de la performance individuelle vers la capacité collective à construire du sens.

C’est peut-être là que les « mathématiques traditionnelles » commencent réellement à mourir : non comme discipline, mais comme régime de production fondé sur la rareté du texte démonstratif.

Ce que l’annonce ne démontre pas

Le modèle utilisé reste interne à OpenAI. L’entreprise publie dix résumés abrégés de raisonnement, des estimations de calcul et des statistiques globales, mais pas un dossier expérimental complet pour chacune des 372 familles. Le public ne peut donc pas reproduire librement l’ensemble du processus ni évaluer précisément l’effet de la sélection, des relances et des interventions humaines.

La publication sur GitHub constitue un progrès par rapport à une simple annonce : les sources sont accessibles, les versions doivent rester consultables et de nombreuses preuves sont accompagnées d’artefacts Lean. Mais le groupe indépendant AGMAI, hébergé par l’Institute for Advanced Study, recommandait aussi un dépôt scientifique indépendant, des identifiants persistants, la publication du modèle, des prompts, du temps et du coût pour chaque résultat, ainsi qu’un état clair des échecs comparables.

Le 6 octobre, ce groupe a qualifié la publication d’événement important pour les mathématiques, tout en précisant que son rôle de conseil ne valait ni approbation du processus ni validation de l’impact des résultats. Sa formule est juste : la mise en ligne est le début, pas l’achèvement, du travail de compréhension humaine.

Les mathématiciens ne servent pas seulement à produire des preuves

Réduire les mathématiques à la résolution de problèmes déjà formulés serait une erreur. La discipline consiste aussi à inventer des concepts, choisir les questions fécondes, construire des ponts entre domaines, reconnaître une idée profonde, simplifier un argument et transmettre une intuition.

Même une machine capable de produire des preuves correctes à la chaîne ne décide pas, à elle seule, de la culture scientifique que nous voulons bâtir. Si seuls quelques laboratoires privés disposent des modèles les plus puissants, ils peuvent aussi influencer les problèmes explorés, le rythme des annonces et les critères de prestige. L’enjeu n’est alors plus seulement intellectuel : il devient institutionnel et politique.

Le mathématicien Daniel Litt a imaginé un risque plus subtil que le remplacement pur et simple : une explosion de résultats que presque personne ne lit, une duplication massive des efforts et des carrières récompensant la production automatisée plutôt que la compréhension. Il ne présente pas ce scénario comme une prédiction et reste optimiste, mais son avertissement touche juste : davantage de théorèmes ne garantit pas davantage de mathématiques comprises.

Alors, est-ce la fin des mathématiques traditionnelles ?

Pas au sens où l’IA aurait clos la discipline. Au contraire, une capacité accrue à explorer des conjectures peut ouvrir de nouveaux territoires. Bryna Kra, interrogée par *WIRED*, résume bien cette position : la manière de travailler va changer, mais ce changement peut aussi permettre de « voir plus grand ».

En revanche, trois piliers sont déjà fragilisés :

1. La preuve comme production rare. Son coût peut chuter spectaculairement.
2. L’article comme unité naturelle de circulation. Des centaines de textes dépassent les capacités ordinaires de relecture.
3. L’accès égal aux instruments. Un modèle privé peut prendre de l’avance sur la communauté qui doit ensuite vérifier ses sorties.

La réponse raisonnable n’est ni de nier le progrès, ni d’accepter une déferlante de manuscrits comme de la connaissance achevée. Il faut de nouvelles institutions : dépôts indépendants, protocoles publics, formalisation, relectures rémunérées, ateliers d’explication et accès plus équitable aux outils.

L’avis d’Elessar Labs

Cette annonce ne signe pas la mort des mathématiques. Elle signe peut-être la fin d’une époque où produire une preuve suffisait à établir une contribution.

Demain, la valeur se déplacera vers la capacité à poser les bonnes questions, à vérifier les correspondances entre preuve formelle et intention scientifique, à dégager une idée intelligible et à la transmettre. Autrement dit, l’IA peut automatiser une part croissante du travail mathématique sans épuiser ce qui fait des mathématiques une activité humaine : comprendre pourquoi un résultat compte.

La rupture est réelle. Mais si les mathématiques traditionnelles désignent la rigueur, la discussion contradictoire et la construction collective du savoir, alors nous n’en avons jamais eu autant besoin.