La revendication d'OpenAI sur Navier-Stokes : une proposition de 166 pages vérifiée sous Lean, construite en 88 heures

OpenAI a déclaré le 8 septembre 2026 qu'un système interne avait produit une proposition pour le problème du millénaire de Navier-Stokes, avec un travail intensif déclenché le 1er septembre, une ébauche analytique le 5 septembre et la vérification Lean achevée le 6 septembre. Pour la piste Navier-Stokes, l'entreprise cite environ 10 000 agents simultanés opérant pendant 88 heures, envoyant 2,7 millions de messages et environ 130 milliards de tokens de sortie, tandis que l'ensemble des tentatives sur les problèmes du millénaire a atteint 4,9 millions de messages et environ 300 milliards de tokens. Le modèle est décrit comme nettement plus capable que GPT-6 Astra, l'article s'intitule Finite Time Blowup for Navier-Stokes et compte 166 pages. L'entreprise présente cette publication comme un rapport d'avancement sur les capacités du modèle, et non comme une revendication de prix, et affirme ne pas avoir l'intention de réclamer le prix d'un million de dollars.

La proposition se présente comme une réfutation visant les alternatives C et D de l'énoncé officiel du Clay Mathematics Institute. Les alternatives A et B demandent une preuve que des données initiales lisses de viscosité positive restent lisses pour toujours, tandis que C et D demandent le contraire : qu'un écoulement incompressible tridimensionnel puisse perdre sa régularité en temps fini. L'affirmation centrale, mise en avant comme Théorème 1.1 dans l'article et résumée par la vidéo, est qu'un fluide partant du repos et restant lisse, lorsqu'il est sollicité par une force extérieure lisse d'énergie finie, peut développer des vitesses qui croissent sans borne à l'approche d'une limite de temps finie conventionnellement notée T égale un. L'annonce, relayée par la BBC et Nature, présente cela comme satisfaisant la formulation précise du problème du millénaire pour toute viscosité positive.

Le tableau physique est celui d'un tourbillon qui s'enroule vers l'intérieur et s'étire verticalement comme des spaghettis, modélisé mathématiquement par des coordonnées de similitude qui se contractent à des rythmes différents radialement et axialement. À mesure que le cœur effilé se rétrécit bien plus vite qu'il ne s'étire, la conservation de la quantité de mouvement force la rotation à s'accélérer, les gradients de pression et les termes de transport croissant ensemble. L'incompressibilité empêche le fluide entrant par les côtés de s'accumuler, le détournant vers un écoulement vertical sortant, si bien que le mouvement vers l'intérieur et l'accélération de la rotation peuvent continuer à s'amplifier. La vidéo traduit les nombres de Reynolds angulaires non bornés de l'article comme une quantité de mouvement submergeant la diffusion visqueuse, ce qui signifie que le fluide effectue un nombre toujours croissant de tours avant que le frottement puisse amortir le mouvement.

Le récit énergétique contre-intuitif est qu'une vitesse non bornée n'implique pas nécessairement une énergie non bornée. Comme la région portant les vitesses extrêmes se rétrécit si vite, son volume tend vers zéro, et l'énergie cinétique intégrée sur tout l'espace reste uniformément bornée. Dans la mise à l'échelle d'ordre dominant de l'article, la contribution du cœur d'explosion à l'énergie totale tend même vers zéro, un point souligné dans le résumé d'OpenAI et dans la narration de la vidéo. Le résultat est un phénomène de concentration plutôt qu'une explosion, ce qui permet à la construction de satisfaire la condition d'énergie finie exigée par l'énoncé du millénaire tout en réalisant l'explosion.

L'ingrédient technique le plus débattu est le caractère forcé de l'explosion et l'affirmation que la force extérieure reste lisse. Plutôt que d'injecter une force infinie ou singulière au moment critique, la construction arrange l'accélération, le gradient de pression, le transport et le frottement visqueux pour que chacun devienne grand tout en s'annulant selon un équilibre détaillé précis, laissant une force résiduelle lisse. L'article décrit cela comme l'ajout d'impulsions spatialement oscillatoires dont les flux de quantité de mouvement non linéaires annulent la partie singulière du résidu. En termes simples, les ondes internes et la quantité de mouvement redistribuent l'énergie croissante de sorte que la poussée extérieurement appliquée demeure lisse même lorsque la vitesse diverge, ce qui est l'exigence difficile qui empêche une triche triviale.

Si elle est vérifiée, la portée est fondamentale plutôt qu'industrielle. Les équations de Navier-Stokes, qui remontent aux travaux de Navier et Stokes au dix-neuvième siècle et servent à la conception d'avions, aux prévisions météorologiques et à l'écoulement sanguin, traitent les fluides comme un milieu continu plutôt que de suivre les molécules individuelles. Une singularité en temps fini avec énergie finie signifierait que cette approximation continue possède un angle mort mathématiquement démontrable : un fluide réel ne peut pas se déplacer à une vitesse infinie, donc au-delà de ce point le modèle continu cesserait d'être un miroir fiable de la réalité et il faudrait suivre le comportement à l'échelle des particules. Comme le notent New Scientist et Nature, la connaissance qu'une telle explosion est possible sous un forçage lisse autorisé redéfinit les limites de la modélisation continue sans fournir pour autant un solveur plus rapide.

La méthode est un arbre de recherche massivement parallèle plutôt qu'un modèle unique réfléchissant pendant 88 heures. OpenAI a d'abord fait tourner environ 1 000 agents pendant 50 heures pour obtenir une réfutation de régularité d'Euler sans forçage, puis a déplacé la puissance de calcul vers Navier-Stokes et est passé à 10 000 agents ; 1 000 agents ont eu besoin de 11 heures pour boucler la dernière étape une fois l'intuition d'Euler en main. Des groupes distincts ont été sollicités avec les variantes A et B pour chercher des preuves de régularité et les variantes C et D pour chercher des réfutations, avec une couche de consolidation de type Codex qui faisait circuler les idées intermédiaires, telles que des astuces d'équilibre de pression, entre des groupes isolés. L'entreprise a estimé que reproduire l'exécution en tant que client coûterait de l'ordre de 15 millions de dollars, et a indiqué que la formalisation et la vérification Lean avaient ajouté 17 heures supplémentaires via GPT-6 Astra, des chiffres répétés lors des briefings de la BBC et de Wired.

La vérification repose sur l'assistant de preuve Lean, qui ne lit pas le PDF comme le ferait un humain mais vérifie les types d'une traduction complète dans le langage formel de Lean. Le pipeline va de l'argument du PDF au théorème formellement énoncé, puis aux dérivations Lean pas à pas, et enfin à la vérification par le noyau que chaque définition, lemme et dépendance découle strictement des axiomes déclarés. Lean agit comme un vérificateur pointilleux qui rejette instantanément tout saut non énoncé, ce qui en fait une preuve plus solide que de demander à un modèle de langage si les 166 pages semblent correctes. Cette force a une limite entre syntaxe et sémantique : une dérivation parfaitement vérifiée d'un énoncé mal formalisé reste une preuve du mauvais énoncé, de sorte que des humains doivent encore auditer si la régularité, le forçage, l'énergie bornée et les alternatives C et D ont été encodés exactement comme la formulation du Clay l'entend, ainsi que les bibliothèques importées et les axiomes.

La chronologie s'est chevauchée avec des travaux menés par des humains et a déclenché un différend de priorité sans preuve établie de copiage. OpenAI affirme que l'entraînement du nouveau modèle interne a commencé le 28 août et que l'essaim a été lancé après avoir appris le 1er septembre que deux problèmes du millénaire avaient été résolus, plus tard compris comme concernant Tristan Buckmaster à NYU et Levent Alpoge chez Anthropic. Buckmaster et Alpoge avaient poursuivi le problème pendant des mois avec Claude et Codex, publiant le 7 septembre une explosion d'Euler à viscosité nulle et notant des progrès sur le cas forcé, tandis qu'une équipe du Caltech dirigée par Anima Anandkumar a annoncé une solution par réseau informé par la physique pour la même variante d'Euler. OpenAI déclare que ni les chercheurs ni les agents n'ont vu ce travail non publié avant la diffusion publique et qu'aucune donnée utilisateur spécifique n'a été consultée, ajoutant la réserve qu'elle ne peut exclure que des données d'utilisation dé-identifiées aient indirectement contribué à améliorer le modèle, et soulignant que les preuves diffèrent et portent respectivement sur des contextes forcé et non forcé.

En pratique, la proposition change peu de choses pour l'ingénierie de demain. Elle ne fournit ni simulateur de fluides universel, ni code de dynamique des fluides numérique plus rapide, ni nouvelles fermetures de turbulence ; les ingénieurs simulent déjà les fluides sous des géométries et conditions aux limites spécifiques avec des méthodes numériques approchées et n'ont pas besoin d'une preuve d'explosion pour concevoir une aile. La valeur immédiate, selon le cadrage d'OpenAI lui-même et le verdict de la vidéo, est l'histoire mathématique et un signal concret que le passage à l'échelle de l'inférence via l'usage multi-agents d'outils peut produire des constructions nouvelles et vérifiables, et pas seulement une meilleure génération de texte. Comme l'a déclaré le président du Clay, Martin Bridson, à New Scientist, l'évaluation sera délibérément sans hâte et rigoureusement vérifiée, de sorte que le problème reste officiellement ouvert en attendant l'examen par les pairs indépendant, un processus que les règles du millénaire lient à au moins deux ans après la publication.