Navier-Stokes : ce que la preuve d'OpenAI par 10 000 agents dit vraiment
Une preuve formalisée en Lean par un modèle interne et une armée d'agents. Une annonce tombée un jour après des travaux concurrents, dans une dispute sur les données Codex.
Le 8 septembre 2026, OpenAI a publié un billet au titre sobre : « On the Navier-Stokes Millennium Prize Problem ». L'entreprise y annonce une preuve analytique, accompagnée d'une formalisation en Lean, selon laquelle un fluide initialement lisse et au repos, soumis à une force lisse, peut développer une singularité en temps fini. Le billet précise que ce résultat établit les énoncés C et D de la formulation officielle du prix du millénaire de l'institut Clay.
Derrière l'annonce se trouve un modèle interne non nommé, décrit comme significativement plus capable que GPT-6 Astra, et environ 10 000 agents logiciels. Mais le même jour, un mathématicien de l'université de New York publiait une déclaration de quatre pages qui raconte une autre histoire : celle d'un effort lancé après la rumeur d'un résultat concurrent, et d'une question restée sans réponse sur les données d'entraînement.
Ce qu'OpenAI a publié exactement
Les équations de Navier-Stokes décrivent le mouvement des fluides en traitant le fluide comme un milieu continu, une approche utilisée pour la conception d'avions, la prévision météorologique ou l'étude de l'écoulement sanguin. La question ouverte depuis environ 90 ans, rappelle le billet : ce modèle continu peut-il se rompre, c'est-à-dire développer des vitesses qui croissent sans borne en temps fini alors même que le mouvement démarre de façon lisse ? Jean Leray avait prouvé en 1934 l'existence de solutions au sens généralisé ; l'institut Clay a inscrit la question parmi ses sept problèmes du millénaire en 2000, chacun doté d'un million de dollars.
La solution annoncée est un vortex : une spirale de fluide qui se resserre, s'allonge « comme des spaghetti » et accélère en gardant une énergie finie, conformément aux lois de la physique. Un point de vocabulaire évite les contresens : dans la formulation officielle rédigée par Charles Fefferman, établir les énoncés C et D revient à réfuter la conjecture affirmative selon laquelle les solutions restent toujours lisses. « Résoudre » signifie ici trancher par la négative, ce que Numerama résumait dans son titre par « une partie d'un problème de maths » et un forum mathématique francophone par « réfuter la conjecture ».
OpenAI publie à la fois le document de la preuve et sa formalisation en Lean. Ce n'est pas sa première incursion du genre : début août, une version interne d'Astra avait déjà produit dix résultats en mathématiques et informatique théorique, et le débat portait déjà sur l'absence de relecteurs extérieurs nommés.
Nous partageons une solution au problème du prix du millénaire de Navier-Stokes, l'un des problèmes les plus profonds aux frontières des mathématiques. La preuve a été produite par un groupe d'agents, à l'aide d'un modèle de nouvelle génération d'OpenAI significativement plus capable que GPT-6 Astra. Le problème : https://openai.com/index/navier-stokes-solution/Voir le post sur X
Dix mille agents pendant 88 heures
Depuis le 28 août, OpenAI entraîne un modèle interne qui montrerait des performances sans précédent dans ses benchmarks, dont les mathématiques ; l'entraînement était toujours en cours au moment de la publication. Le 1er septembre, l'entreprise entend une rumeur : deux problèmes du millénaire viendraient d'être résolus. Elle décide alors d'évaluer son modèle sur l'ensemble des problèmes du millénaire et quelques autres questions à fort impact.
Le dispositif : des groupes d'agents communicants, dotés d'une version en cache d'internet et de l'exécution de code, chaque groupe recevant une variante de l'énoncé (A et B pour les formes qui mèneraient à une preuve, C et D à une réfutation). Le groupe affecté à Navier-Stokes comptait de l'ordre de 10 000 agents simultanés. La première surprise est venue d'un problème jugé plus simple : la régularité des équations d'Euler dans leur version non forcée, obtenue par une centaine d'agents en une cinquantaine d'heures. OpenAI a alors concentré ses ressources sur Navier-Stokes, résolu le samedi 5 septembre environ 88 heures après le lancement, puis formalisé et vérifié en Lean en 17 heures supplémentaires via GPT-6 Astra, le modèle lancé début septembre. Sur l'ensemble des problèmes tentés, les agents ont échangé 4,9 millions de messages et produit environ 300 milliards de jetons de sortie, une valeur de 22,5 millions de dollars aux tarifs actuels d'Astra selon l'estimation de TechCrunch.
La dispute sur la paternité et les données Codex
La rumeur du 1er septembre, OpenAI l'a comprise après coup : elle concernait Levent Alpöge, mathématicien employé par Anthropic, et Tristan Buckmaster, professeur à NYU. Le duo travaillait depuis un an sur la piste même que le billet dit avoir suivie : l'explosion en temps fini par forçage lisse, les options C et D de Fefferman. « Ce n'est pas la direction à laquelle on arrive en quelques jours en donnant l'énoncé du problème à un modèle », écrit Buckmaster, pour qui entendre « forcé » a été « un signal d'alarme écarlate ».
Sa déclaration détaille : le 3 septembre, il écrit à un mathématicien éminent d'OpenAI pour lui donner les faits. Le 6, deux appels avec Sébastien Bubeck. On lui montre un prompt et on lui affirme un très faible apport humain ; au fil de l'échange, il apprend qu'une équipe entière travaillait le sujet, que l'effort avait commencé par le problème non forcé et des questions plus simples, et qu'une quantité de calcul « délirante » a été mobilisée. Sur la question qui fâche, l'entraînement éventuel du modèle sur leurs sessions Codex, où les deux chercheurs déposaient leurs brouillons depuis un an (l'outil est décrit dans notre fiche Codex), il n'obtient pas de réponse.
| Acteur | Résultat rendu public | Statut au 9 septembre |
|---|---|---|
| OpenAI | Navier-Stokes (énoncés C et D), Euler non forcé | Preuve et formalisation Lean publiées le 8 septembre |
| Alpöge et Buckmaster | Euler 3D forcé, Boussinesq, milieux poreux | Publiés le 7 septembre, d'après The Verge |
| Alpöge et Buckmaster | Navier-Stokes hypo-dissipatif | Non publié : vérification Lean inachevée selon leur déclaration |
Le billet d'OpenAI répond à sa manière : aucun accès à des données d'utilisateurs spécifiques pour résoudre le problème, mais « bien que peu probable, nous ne pouvons pas exclure que des données déidentifiées dérivées de leur usage de nos produits aient aidé à améliorer nos modèles ». Sur Mastodon, Buckmaster y lit un aveu : OpenAI « admet ouvertement avoir utilisé des données d'entraînement d'une période postérieure à la découverte de notre résultat », rapporte The Verge. Sam Altman, dans un post X, conteste toute faute : l'équipe a agi avec intégrité selon lui, une annonce conjointe avait été proposée, et le duo a proféré des « accusations de plagiat infondées ». Sébastien Bubeck a répondu point par point :
J'aimerais clarifier quelques points : 1) La capture d'écran correspond à ma prise de contact avec Levent pour coordonner nos publications respectives. J'espère qu'il ressort clairement du message que nous sommes venus avec les meilleures intentions possibles. 2) Je n'ai jamais, jamais demandé que Levent soit retiré de la paternité de son propre travail.Voir le post sur X
Buckmaster se défend lui-même d'accuser qui que ce soit : « Je n'ai pas vu la preuve d'OpenAI. Je ne sais pas si nos données ont été utilisées. Je n'accuse personne de rien. »
« Résolu » au sens où l'entend OpenAI
Le billet écrit que le résultat « résout » le problème en établissant les énoncés C et D. Mais OpenAI précise ne pas avoir l'intention de réclamer le prix du millénaire, et aucune validation par l'institut Clay ou par des relecteurs extérieurs nommés n'avait été annoncée au moment de la publication. La formalisation Lean, publique, permet une vérification mécanisée ; l'examen par la communauté mathématique ne fait que commencer.
Ce que l'annonce dit surtout, c'est la vitesse. Le modèle utilisé n'est disponible nulle part : il est interne, en cours d'entraînement, et OpenAI le présente comme un signal du rythme à venir. Après les dix résultats d'Astra en août et l'avancée de Claude sur l'hypothèse de Riemann, le motif se répète : des annonces plus rapides, des preuves plus automatisées, et un débat récurrent sur la vérification. Buckmaster, lui, situe l'enjeu ailleurs : le fait qu'un mathématicien et un modèle de langage puissent faire tout ce travail en un mois change la formation, l'attribution du crédit et l'évaluation scientifiques, écrit-il en comparant le moment à Deep Blue contre Kasparov.
Si un modèle d'OpenAI a vraiment comblé le vide jusqu'à Navier-Stokes, c'est une chose remarquable, et elle devrait être dite à voix haute, par eux, avec l'histoire intacte.Tristan Buckmaster, déclaration du 8 septembre 2026
Questions fréquentes
OpenAI a-t-il résolu le problème de Navier-Stokes ?
L'entreprise annonce une preuve, formalisée en Lean, des énoncés C et D de la formulation Clay : un fluide lisse au repos peut développer une singularité en temps fini. Elle écrit ne pas vouloir réclamer le prix, et la validation par la communauté mathématique reste à venir.
Quel modèle a produit la preuve ?
Un modèle interne non nommé, décrit comme significativement plus capable que GPT-6 Astra, dont l'entraînement a commencé le 28 août et était toujours en cours à la publication.
Pourquoi une controverse ?
L'effort d'OpenAI a démarré le 1er septembre, après la rumeur d'un résultat des mathématiciens Alpöge et Buckmaster, qui travaillaient dans Codex. OpenAI dit qu'aucune donnée spécifique n'a été consultée, mais ne peut exclure que des données déidentifiées aient amélioré ses modèles.
Qui peut toucher le million de dollars du Clay ?
Rien n'est engagé pour l'instant : OpenAI écrit ne pas avoir l'intention de réclamer le prix, et le duo Alpöge-Buckmaster a publié des résultats sur Euler, un problème connexe.
