Un tourbillon qui se resserre jusqu’à devenir infiniment rapide, tout en gardant une énergie totale finie : c’est le mécanisme au cœur d’une proposition de preuve publiée par OpenAI le 8 septembre 2026. Le groupe affirme qu’un système interne d’intelligence artificielle a résolu le problème d’existence et de régularité des équations de Navier–Stokes, l’un des sept problèmes du millénaire dotés chacun d’un prix d’un million de dollars.
Le résultat est accompagné d’un article de 166 pages et d’une formalisation dans le langage Lean, dont les fichiers sont publics. Il ne s’agit donc pas d’une réponse énigmatique produite par un chatbot, mais d’un objet mathématique détaillé que des spécialistes peuvent lire et qu’un logiciel peut contrôler ligne par ligne.
Cela ne signifie pas que le problème est officiellement résolu. La démonstration n’a pas encore reçu l’acceptation générale de la communauté mathématique, le Clay Mathematics Institute ne l’a pas validée et OpenAI ne réclame pas le prix. Une controverse de priorité complique en outre le récit : des chercheurs humains travaillaient depuis plusieurs années sur la stratégie mathématique qui a ouvert cette voie et utilisaient eux-mêmes des modèles d’IA.
L’événement demeure potentiellement historique. Il montre surtout que la recherche assistée par IA change d’échelle : environ 10 000 agents, 130 milliards de tokens de sortie et 88 heures d’exploration ont été mobilisés pour produire une preuve candidate qu’aucune équipe humaine n’aurait pu examiner aussi vite sans formalisation.
Le problème ne demande pas de calculer tous les fluides
Les équations de Navier–Stokes décrivent le mouvement de l’eau, de l’air et d’autres fluides en combinant l’accélération, la pression, le transport de la quantité de mouvement et la viscosité. Elles servent en aéronautique, en météorologie ou dans l’étude de la circulation sanguine. Les ingénieurs savent depuis longtemps les approcher numériquement pour des situations concrètes.
Le problème du millénaire pose une question différente. À partir d’un mouvement initial parfaitement lisse en trois dimensions, ces équations produisent-elles toujours une solution régulière pour toute la durée de l’évolution ? Ou peuvent-elles conduire, en temps fini, à une singularité où la vitesse ou ses dérivées deviennent sans limite ?
La difficulté vient d’une compétition. La viscosité tend à lisser les variations du fluide, comme une friction interne. Le terme non linéaire qui transporte le mouvement peut, au contraire, concentrer la rotation et transférer de l’énergie entre les échelles. En deux dimensions, les mathématiciens contrôlent cette dynamique. En trois dimensions, l’étirement des tourbillons rend le comportement beaucoup plus difficile à borner.
Jean Leray a démontré en 1934 l’existence globale de solutions dites faibles, capables de représenter le mouvement de manière moyenne. Mais une solution faible peut perdre la régularité ou l’unicité. Le défi consiste précisément à savoir si une donnée initiale lisse reste lisse ou si un effondrement mathématique peut apparaître.
Ce que la preuve d’OpenAI affirme exactement
OpenAI ne prétend pas montrer que tous les fluides ordinaires deviennent singuliers. La construction décrit un cas soigneusement choisi : un fluide incompressible tridimensionnel, initialement au repos, auquel est appliquée une force extérieure lisse, localisée dans l’espace et dans le temps.
Le champ de vitesse forme un vortex qui tourne, se contracte radialement et s’étire verticalement. À mesure que son cœur rétrécit, la vitesse augmente jusqu’à devenir non bornée à un instant fini, fixé à 1 dans la construction. Son énergie cinétique totale reste pourtant bornée. La force appliquée reste elle aussi lisse : la singularité ne peut donc pas être attribuée à une impulsion extérieure infinie introduite artificiellement.
Le point technique décisif consiste à faire diverger plusieurs termes de l’équation tout en organisant leur annulation. Des impulsions oscillatoires produisent un flux de quantité de mouvement qui compense les erreurs singulières laissées par le vortex principal. Une série de corrections élimine ensuite les résidus jusqu’à obtenir une force régulière.
La preuve revendique les alternatives C et D de la formulation officielle de Charles Fefferman : l’effondrement pour l’espace entier en trois dimensions et pour le tore périodique. Le dépôt Lean résume le résultat ainsi : pour toute viscosité positive, il existe des données initiales et une force lisses pour lesquelles aucune solution globale lisse répondant aux conditions d’énergie demandées ne subsiste.
Pourquoi la force extérieure n’est pas un détail disqualifiant
L’expression « avec force » peut sembler plus faible que le problème souvent résumé au grand public comme un fluide laissé à lui-même. La formulation du Clay prévoit pourtant explicitement des variantes avec une force extérieure régulière. Une démonstration correcte des cas C ou D suffit donc, en principe, à trancher le problème par un contre-exemple.
La contrainte importante est la régularité de cette force. Il serait facile de définir après coup une sollicitation aussi irrégulière que le mouvement recherché. Ici, toute la construction vise à produire une vitesse qui explose alors que la force demeure infiniment dérivable. C’est ce verrou qui transforme un vortex spectaculaire en candidat sérieux au problème du millénaire.
Le résultat ne dit pas non plus qu’un avion, un océan ou le sang humain atteindra réellement une vitesse infinie. Une singularité indique que le modèle continu cesse de décrire la situation à cette échelle. Les fluides physiques sont composés de molécules et d’autres effets interviennent bien avant l’infini mathématique.
Dix mille agents et 88 heures de recherche
Le processus décrit par OpenAI ressemble moins à une conversation qu’à une campagne de calcul scientifique. Le 1er septembre, après avoir entendu des rumeurs sur des avancées concernant deux problèmes du millénaire, l’entreprise a lancé son modèle interne sur les problèmes encore ouverts et sur plusieurs variantes plus accessibles.
Les agents ont été répartis en groupes capables de communiquer en interne. Ils pouvaient consulter une copie mise en cache du Web et exécuter du code. Certaines équipes cherchaient à prouver la régularité, d’autres à construire un contre-exemple. OpenAI explique avoir encouragé des approches différentes, puis utilisé Codex pour consolider les pistes les plus prometteuses entre les groupes.
Une première percée est venue d’un problème voisin : les équations d’Euler, qui correspondent au cas sans viscosité. Le système aurait trouvé une singularité en temps fini pour la version non forcée. Les agents travaillant sur Navier–Stokes ont ensuite reçu ce résultat intermédiaire et une version plus récente du modèle interne.
La construction finale est apparue après environ 88 heures. Sa formalisation et sa vérification dans Lean ont demandé 17 heures supplémentaires avec GPT-6 Astra. Pour la seule recherche Navier–Stokes, les agents ont produit environ 2,7 millions de messages et 130 milliards de tokens de sortie, selon OpenAI. L’entreprise a évoqué auprès d’Axios un coût de calcul de plusieurs millions de dollars.
Ces chiffres décrivent une force brute organisée, pas une intuition isolée. Le système a exploré de nombreux chemins, partagé des résultats et consacré un volume de calcul inaccessible à un mathématicien individuel. Les humains n’ont pas disparu du processus : ils ont choisi les problèmes, organisé les groupes, injecté les résultats intermédiaires, consolidé les idées et décidé ce qui méritait une formalisation.
Lean vérifie la logique, pas toute la science autour
Lean est un assistant de preuve. Chaque définition et chaque étape doivent être traduites dans un langage formel, puis vérifiées par un petit noyau logiciel. Si le programme compile sans utiliser d’axiomes indésirables ni laisser de trous, il offre une garantie bien plus forte qu’une simple relecture automatique par un modèle de langage.
Le dépôt public d’OpenAI contient les fichiers Lean consacrés à Navier–Stokes et à Euler, la version de l’outil utilisée et les instructions de compilation. Des équipes externes peuvent donc reconstruire le certificat. Cette reproductibilité est essentielle pour une preuve de 166 pages, où une erreur discrète peut invalider tout un argument.
La formalisation ne clôt toutefois pas l’examen. Les spécialistes doivent vérifier que les définitions formelles correspondent bien à la formulation du Clay, que les hypothèses encodées sont celles annoncées dans l’article et que le théorème prouvé couvre sans glissement les alternatives C et D. Il faut aussi rendre l’argument intelligible : une preuve correcte mais opaque transmet moins de compréhension et rend plus difficile la détection d’un mauvais cadrage.
Un vérificateur formel atteste que les conclusions suivent des prémisses inscrites dans le système. Il ne décide pas à lui seul que ces prémisses représentent exactement la question historique que la communauté voulait résoudre.
Pourquoi le million de dollars n’est pas encore attribué
Les règles du Clay Mathematics Institute sont volontairement lentes. L’institut n’accepte pas les soumissions directes. Une solution doit d’abord être publiée dans une revue ou un support qualifié, puis rester accessible à l’examen pendant au moins deux ans et recevoir l’acceptation générale de la communauté mathématique avant même d’être considérée.
Le billet d’OpenAI, le PDF et le certificat Lean constituent une publication publique, mais pas une validation institutionnelle. Des experts devront reconstruire la formalisation, relire la preuve analytique et débattre de sa conformité exacte. À la date de cet article, aucune évaluation indépendante complète n’a été rendue publique.
OpenAI déclare ne pas vouloir réclamer le prix. Ce choix ne dispense pas la preuve du même niveau d’examen. La question la plus importante n’est pas l’identité du bénéficiaire du million de dollars, mais la possibilité pour la communauté de reconnaître le résultat comme un théorème fiable et de comprendre les idées qu’il apporte.
Une controverse sur la route suivie et le crédit
L’histoire mathématique ne commence pas le 1er septembre. Diego Córdoba et Luis Martínez-Zoroa développaient depuis plusieurs années une stratégie fondée sur une cascade de couches de vorticité à des échelles de plus en plus petites. Tristan Buckmaster, professeur à l’université de New York, et Levent Alpöge, chercheur chez Anthropic travaillant à titre personnel, ont repris ce programme avec l’aide de plusieurs modèles d’IA.
Le duo a annoncé des singularités en temps fini avec force lisse pour trois systèmes voisins, dont les équations d’Euler tridimensionnelles. Buckmaster attribue explicitement l’idée fondamentale à Córdoba et Martínez-Zoroa. Il explique aussi que la première preuve générée par un modèle était très difficile à lire et qu’elle a été vérifiée dans Lean avant que les chercheurs ne cherchent à la rendre compréhensible.
La dispute porte sur ce qui s’est passé ensuite. OpenAI reconnaît avoir commencé son effort après avoir entendu une rumeur liée aux travaux de Buckmaster et Alpöge. Buckmaster affirme que cette information a orienté l’entreprise vers une voie très spécifique et raconte avoir été pressé de publier rapidement, avec une proposition qui aurait exclu Alpöge de la signature en raison de son emploi chez Anthropic. Il précise ne pas avoir vu la preuve d’OpenAI, ne pas savoir si leurs données ont été utilisées et ne pas porter d’accusation formelle de plagiat.
OpenAI affirme qu’aucun chercheur ni agent n’a consulté leurs travaux avant leur publication. Après une enquête interne, l’entreprise a ajouté le 10 septembre que les prompts Codex de Buckmaster pendant les deux mois précédents ne pouvaient pas avoir influencé le système, y compris par l’entraînement, et que les deux preuves différaient sensiblement.
Ces versions ne suffisent pas à régler toutes les questions d’attribution. Une idée peut circuler par une rumeur sans qu’un document privé soit copié. Une entreprise qui fournit des outils aux chercheurs peut aussi mobiliser, dès qu’elle apprend qu’une percée approche, des moyens que ses clients ne possèdent pas. Même si la preuve d’OpenAI est indépendante au sens technique, la chronologie oblige les laboratoires à définir des règles claires sur la confidentialité, la provenance des pistes et le crédit accordé aux travaux précurseurs.
La prochaine révolution scientifique sera aussi institutionnelle
Si la preuve résiste à l’examen, la performance ne tiendra pas seulement à la résolution d’un vieux problème. Elle montrera qu’un système multi-agent peut parcourir une littérature, explorer simultanément des milliers de variantes, assembler une stratégie et produire un certificat formel sur un problème au sommet des mathématiques.
Ce mode de recherche déplace les goulets d’étranglement. Générer des pistes devient moins rare ; choisir les bonnes, les formaliser, les rendre lisibles et attribuer correctement le mérite devient plus important. La quantité de calcul devient également un facteur scientifique : une équipe dotée de millions de dollars peut transformer une rumeur en campagne massive avant que les auteurs humains d’une idée aient terminé leur manuscrit.
Le résultat Navier–Stokes doit donc subir deux vérifications parallèles. La première est mathématique : la preuve établit-elle réellement les alternatives annoncées ? La seconde est institutionnelle : la recherche assistée par IA peut-elle conserver des règles de confiance, de confidentialité et de priorité lorsque le fournisseur de l’outil devient aussi un concurrent ?
Lean peut certifier une chaîne logique. Il ne peut pas décider seul qui a ouvert la voie, comment partager le crédit ni quand une communauté a suffisamment compris un résultat pour le déclarer acquis. C’est désormais à la communauté mathématique de faire ce travail — lentement, publiquement et sans confondre la vitesse de génération avec la vitesse de validation.
Références
- OpenAI — proposition de solution au problème de Navier–Stokes, 8 septembre 2026, mise à jour le 10 septembre
- OpenAI — article complet Finite Time Blowup for Navier–Stokes
- OpenAI — certificats Lean pour Navier–Stokes et Euler
- Clay Mathematics Institute — présentation officielle du problème de Navier–Stokes
- Clay Mathematics Institute — règles des problèmes du millénaire
- Tristan Buckmaster — déclaration sur les résultats, la chronologie et l’attribution
- Axios — proposition de preuve et controverse de priorité, 8 septembre 2026
- El País — origine de la stratégie et réactions de Diego Córdoba et Luis Martínez-Zoroa, 10 septembre 2026
