Le 8 septembre 2026, OpenAI a annoncé une proposition de preuve concernant Navier–Stokes, accompagnée d’une formalisation Lean. L’entreprise revendique la résolution des formulations C et D du problème du millénaire. [1] Il faut distinguer cette annonce de l’attribution officielle du prix : au moment de notre consultation, la page du Clay Mathematics Institute affiche toujours le problème comme actif. [3]
Que décrivent les équations de Navier–Stokes ?
Elles décrivent le mouvement des fluides, notamment l’eau et l’air. Leur intérêt dépasse une abstraction mathématique : les écoulements et la turbulence concernent des phénomènes observables au quotidien. Le défi théorique consiste à préciser les conditions dans lesquelles les solutions restent bien définies. [3]
Une image aide à comprendre l’enjeu : un logiciel peut dessiner une trajectoire plausible, mais une démonstration doit établir pourquoi une propriété reste vraie sous les hypothèses annoncées. L’apparence convaincante d’un résultat ne remplace donc pas son fondement logique.
∇ · u = 0Forme incompressible à densité normalisée : vitesse u, pression p, viscosité ν, force extérieure f. [4]
Le texte officiel distingue quatre formulations. Les versions A et B portent sur l’existence de solutions lisses sans force extérieure ; les versions C et D autorisent une force lisse pour établir un cas de rupture. Le domaine peut être l’espace entier ou un domaine périodique. [4]
Qu’affirme exactement la preuve proposée ?
Le manuscrit construit un écoulement tridimensionnel qui part du repos, sous une force extérieure lisse, et dont la vitesse devient non bornée en temps fini. L’énergie cinétique reste bornée. Le théorème annoncé vaut pour toute viscosité strictement positive ; la force a un support compact dans l’espace et le temps. Le PDF compte 166 pages. [2]
Ces qualifications déterminent la portée du résultat. « Avec forçage » ne signifie pas automatiquement « hors sujet » : les formulations C et D prévoient justement cette possibilité. En revanche, cette construction ne constitue pas une démonstration d’explosion pour le cas sans forçage. [4]
| Ce que présente le manuscrit | Ce qu’il ne faut pas en déduire |
|---|---|
| Une construction de rupture sous des hypothèses précises. | Une formule universelle prédisant tous les fluides. |
| Une vitesse non bornée avec énergie bornée. | Une expérience montrant de l’eau réellement infiniment rapide. |
| Un résultat avec force extérieure lisse. | La résolution automatique du cas sans force. |
Lecture pédagogique de l’énoncé du manuscrit [2], et non expertise indépendante de sa démonstration complète.
Parler d’une « proposition de preuve sur Navier–Stokes » permet de transmettre l’importance de l’annonce tout en laissant visible son statut scientifique.
Comment les agents IA ont-ils travaillé ?
OpenAI décrit une recherche coordonnée à grande échelle. Des groupes exploraient différentes pistes, utilisaient du code et un accès à une version mise en cache du Web. Codex aidait à consolider les résultats intermédiaires. Le modèle de recherche était interne, présenté comme plus capable que GPT-6 Astra. [1]
Chiffres déclarés par OpenAI. Navier–Stokes : 2,7 millions de messages et environ 130 milliards de tokens de sortie. Tous les problèmes explorés : 4,9 millions de messages et 300 milliards de tokens de sortie. [1]
Notre lecture : la coordination mérite autant d’attention que le nombre d’agents. Multiplier les réponses peut multiplier les erreurs identiques. Une organisation utile doit préserver les désaccords, repérer les impasses et transmettre les résultats exploitables aux autres groupes.
Une percée à plusieurs millions de dollars ?
Les volumes de calcul ne constituent pas une facture publique. Nous ne disposons pas, dans les documents examinés, d’un coût complet vérifiable. Un modèle interne n’a pas nécessairement le même coût que le tarif commercial d’une API.
Pour comprendre les ordres de grandeur, voici une simple simulation arithmétique fondée sur le volume de sortie indiqué plus haut. Les prix unitaires sont des hypothèses pédagogiques, pas les tarifs du système utilisé.
| Prix hypothétique / million de tokens de sortie | Montant pour 130 milliards |
|---|---|
| 10 dollars | 1,3 million de dollars |
| 25 dollars | 3,25 millions de dollars |
| 50 dollars | 6,5 millions de dollars |
Calcul : 130 000 millions de tokens × prix unitaire. Hors tokens d’entrée, entraînement, outils, infrastructure et travail humain. Ces montants ne sont ni une estimation validée ni une borne du coût réel.
Pour un entrepreneur, la leçon est budgétaire : un système autonome doit disposer d’un plafond de dépenses et d’une condition d’arrêt. Une tâche qui s’exécute plus longtemps n’apporte pas nécessairement une valeur proportionnelle.
Pourquoi Lean change-t-il la vérification ?
Lean est un assistant de preuve, pas un second chatbot qui donne son avis. Il permet d’écrire des énoncés et des démonstrations dans un langage formel. Son noyau vérifie les étapes logiques dans le cadre des définitions et hypothèses utilisées. [6]
Cette distinction est centrale : demander à une autre IA « est-ce correct ? » reste une évaluation en langage naturel. Une vérification formelle cherche à rendre les dépendances logiques explicites et contrôlables. Elle ne dispense cependant pas de vérifier que l’énoncé formalisé correspond bien à la question scientifique initiale.
Le dépôt public d’OpenAI contient des formalisations Lean 4 pour Navier–Stokes et Euler. Son README documente la compilation et renvoie à des instructions de contrôle indépendant avec Comparator. Nous avons consulté cette documentation ; nous n’avons pas recompilé ni audité l’ensemble de la preuve. [5]
Et la validation du prix du millénaire ?
Le Clay Mathematics Institute exige notamment une publication dans un support admissible, un délai d’au moins deux ans après cette publication et une acceptation générale par la communauté mathématique. L’institut n’accepte pas de soumission directe. [7] OpenAI indique ne pas vouloir réclamer le prix. [1]
Que retenir pour la recherche et les entreprises ?
Notre analyse : la valeur se situe dans l’association entre exploration et contrôle. L’enseignement pratique n’est pas de reproduire l’échelle de ce projet, mais d’organiser des tâches dont le résultat peut être vérifié.
Recherche scientifique
Conserver les hypothèses, les expériences infructueuses et les versions des démonstrations. Une piste utile doit pouvoir être examinée par d’autres.
Développement logiciel
Demander une modification accompagnée d’un test pertinent, puis vérifier le comportement attendu. La quantité de code générée ne mesure pas la qualité.
Analyse de données
Associer chaque conclusion au calcul qui la soutient. Distinguer les observations, les hypothèses et les extrapolations commerciales.
Création de contenu
Utiliser l’IA pour structurer une enquête, puis contrôler les sources, dates et chiffres. Un texte convaincant doit rester traçable.
La question de la confiance entre chercheurs et laboratoires
Au-delà de ce cas, nous considérons la traçabilité des contributions comme un enjeu de conception : qui propose une idée, qui l’exploite, qui la vérifie et comment cette contribution est-elle reconnue ? Un outil scientifique doit faciliter ces réponses.
Une avancée à lire avec précision
Ce dossier mérite mieux qu’une opposition entre enthousiasme et rejet. Le bon réflexe consiste à ouvrir l’énoncé, identifier les hypothèses et examiner les éléments contrôlables. Pour suivre l’IA scientifique, la question la plus utile devient : « Qu’a-t-on exactement établi, et comment puis-je le vérifier ? »
Cet article est un décryptage documentaire. Il ne constitue pas une validation mathématique indépendante ni une reproduction de l’expérience informatique.
Questions fréquentes
Résoudre un cas de Navier–Stokes suffit-il à prédire tous les fluides ?
Non. Un théorème porte sur un énoncé délimité. Il faut ensuite établir séparément ses conséquences pour une application concrète, ses conditions d’utilisation et ses limites.
Une visualisation de vortex est-elle une preuve ?
Non. Une illustration explique une idée ; une simulation calcule une approximation ; une preuve établit un résultat sous des hypothèses. Les visuels de cet article sont pédagogiques ou artistiques.
Peut-on reproduire ce projet avec un abonnement ChatGPT ?
Un abonnement grand public ne garantit pas l’accès au même modèle, à la même orchestration ni au même budget de calcul. Il serait trompeur de promettre une reproduction à partir d’un simple prompt.
Plus d’agents signifie-t-il de meilleurs résultats ?
Pas automatiquement. Il faut mesurer les erreurs, le coût de coordination et la qualité finale. Plusieurs agents peuvent converger vers la même mauvaise hypothèse.
Comment suivre la suite de cette annonce ?
Consultez le manuscrit, l’historique du dépôt de preuve, les mises à jour de l’annonce et les informations officielles du Clay Mathematics Institute. Les liens directs figurent ci-dessous.
Sources et méthode
Sources primaires consultées le 11 septembre 2026. Les chiffres de fonctionnement sont attribués à OpenAI ; les simulations de coût et les recommandations pratiques relèvent de notre analyse.
- OpenAI — On the Navier–Stokes Millennium Prize Problem. Annonce du 8 septembre 2026, section sur les travaux concurrents mise à jour le 10 septembre.
- OpenAI — Finite time blowup for Navier–Stokes. Manuscrit, résumé et théorème 1.1 ; 166 pages.
- Clay Mathematics Institute — Navier–Stokes Equation. Présentation et statut affiché du problème.
- Charles L. Fefferman — Existence and Smoothness of the Navier–Stokes Equation. Formulation officielle, notamment variantes A à D.
- OpenAI — dépôt NavierStokesAndEuler. Formalisations et instructions de vérification.
- Lean — site officiel. Présentation du langage et de l’assistant de preuve.
- Clay Mathematics Institute — règles des problèmes du millénaire. Conditions d’examen d’une solution proposée.
