Navier–Stokes : la preuve d’OpenAI attend encore son verdict scientifique
Dans sa publication du 8 septembre 2026, OpenAI affirme avoir démontré qu’une solution initialement lisse des équations tridimensionnelles de Navier–Stokes peut devenir singulière en temps fini sous l’effet d’une force extérieure lisse. L’entreprise a diffusé une démonstration analytique et sa formalisation dans Lean.
La publication du 8 septembre demeure toutefois une proposition de preuve, et non un résultat déjà consacré par la communauté mathématique. Le premier bilan de Numerama relève qu’aucun examen scientifique extérieur n’avait encore validé le résultat et que le contrôle de Lean ne suffit pas à établir son acceptation générale.
Ce que la démonstration cherche à établir
La proposition concerne un fluide incompressible en trois dimensions, initialement lisse et au repos. Une force extérieure, elle aussi lisse, agit sur ce fluide jusqu’à ce que sa vitesse devienne non bornée en un temps fini, tandis que son énergie reste finie.
La construction prend la forme d’un vortex qui tourne, se resserre vers l’intérieur et s’allonge. À mesure que sa région centrale rétrécit, la vitesse augmente. Le point délicat consiste à obtenir cette rupture par la dynamique des équations tout en conservant une force régulière, plutôt qu’en introduisant artificiellement une force déjà singulière.
La présence d’une force extérieure ne place pas automatiquement le résultat hors du problème du millénaire. Les énoncés « C » et « D » de sa formulation officielle autorisent une force lisse et demandent précisément de construire des données pour lesquelles aucune solution lisse globale n’existe. La portée revendiquée est donc existentielle : il suffirait d’un tel contre-exemple, et non d’une explosion de toutes les solutions.
Cette singularité est un objet mathématique. Elle signifierait que la vitesse décrite par le modèle croît sans limite en un temps fini, pas qu’un fluide réel pourrait atteindre une vitesse infinie. Si l’argument est correct, il montrerait plutôt l’endroit où la description continue du fluide cesse de rester régulière.
Une recherche massive, puis une formalisation distincte
Le processus décrit mobilise de l’ordre de 10 000 agents coordonnés. Ceux-ci auraient abouti à la démonstration environ 88 heures après le lancement de l’expérience ; 17 heures supplémentaires auraient servi à sa formalisation et à sa vérification dans Lean avec GPT‑6 Astra.
Cette chronologie sépare deux opérations. Le système multiagent a produit l’argument analytique, rédigé dans le langage des mathématiques, puis un autre travail a traduit cet argument en objets et étapes que Lean peut contrôler. La formalisation n’est donc pas seulement une copie mise en page : elle constitue une seconde représentation du théorème et de sa preuve.
Cette distinction importe aussi pour attribuer exactement le résultat. Le modèle interne qui alimentait les agents est présenté comme plus performant que GPT‑6 Astra ; ce dernier est associé à l’étape ultérieure de formalisation. Attribuer toute la découverte à GPT‑6 Astra confondrait les deux phases annoncées.
Ce que Lean vérifie — et ce qu’il ne décide pas
Lean contrôle qu’une suite d’étapes formelles découle des définitions, axiomes et résultats admis dans le projet. Ce mécanisme réduit fortement le risque qu’un calcul faux ou qu’un saut logique passe inaperçu dans la version formalisée.
Il ne décide cependant pas, à lui seul, que le fichier formalise exactement le problème historique. Des spécialistes doivent encore comparer les définitions avec l’énoncé visé, vérifier que toutes les hypothèses analytiques ont été correctement traduites et s’assurer que le théorème contrôlé par la machine possède bien la portée annoncée.
La validation logique et le verdict scientifique répondent donc à deux questions différentes. La première demande si le code de preuve est accepté dans un cadre formel déterminé. Le second exige une reconstruction indépendante de l’argument, une comparaison entre le manuscrit et le fichier Lean, puis une appréciation par les spécialistes des équations aux dérivées partielles.
Même une preuve formellement exécutable ne vaut pas reconnaissance institutionnelle immédiate. Le Clay Mathematics Institute n’a pas déclaré le problème résolu : sa procédure suppose notamment une publication admissible, un délai d’au moins deux ans et une acceptation générale dans la communauté avant l’examen d’une solution pour le prix.
La priorité scientifique forme un dossier séparé
La controverse implique Tristan Buckmaster, mathématicien à la New York University, et Levent Alpöge, chercheur chez Anthropic. Leur travail concernait une singularité pour les équations d’Euler forcées, proches de Navier–Stokes mais dépourvues du terme de viscosité ; le résultat présenté par le système d’OpenAI pour Euler porte, lui, sur une variante non forcée.
Buckmaster a soutenu que des recherches privées antérieures avaient orienté la course et s’est interrogé sur une éventuelle influence de notes ou de requêtes confiées à Codex. L’enquête d’El País du 9 septembre expose ces accusations, les démentis opposés par l’entreprise et l’absence de vérification indépendante de la preuve à cette date.
Ces accusations ne constituent pas des faits établis. Le désaccord porte sur l’accès éventuel à des travaux non publiés, l’origine de certaines idées et les conditions dans lesquelles une publication commune a été discutée. Il ne permet pas, dans un sens ou dans l’autre, de conclure à la validité mathématique de la démonstration.
Quatre questions restent ainsi distinctes : le manuscrit analytique est public ; sa formalisation Lean l’est également ; leur adéquation au problème et leur correction doivent encore être examinées indépendamment ; enfin, la priorité et l’attribution font l’objet d’un conflit non tranché. Le verdict dépendra des analyses détaillées du manuscrit et du code formel, pas de la seule annonce ni de la controverse qui l’accompagne.
À lire aussi:
Abonnez-vous à notre newsletter
Recevez directement les dernières actualités sur le Web3, l’IA et les cryptomonnaies.