La revendication d’OpenAI sur une preuve de Navier–Stokes, expliquée

Les équations de Navier–Stokes décrivent le mouvement des fluides, comme l’eau et l’air. Elles sont au cœur de la dynamique des fluides, de l’ingénierie et de la physique, mais les mathématiciens ne disposent toujours pas d’une compréhension analytique complète de leur comportement en trois dimensions.

La version du prix du millénaire demande, en résumé, si des conditions initiales lisses conduisent toujours à des solutions lisses pour tout temps futur, ou si les équations peuvent « exploser » — en produisant une singularité où une quantité, comme la vitesse, devient infinie. Le Clay Mathematics Institute a désigné ce problème comme l’un des sept problèmes du prix du millénaire en 2000, chacun associé à un prix de $1 million. Avant cette annonce, seule la conjecture de Poincaré avait été résolue parmi les sept, comme le résume Wikipedia.

La revendication d’OpenAI, telle que rapportée par Quanta Magazine, est que des agents d’IA autonomes exécutés sur un modèle interne ont trouvé une singularité dans les équations de Navier–Stokes tridimensionnelles. Quanta rapporte que le travail a utilisé environ 10 000 agents, que les agents ont trouvé une preuve après 88 heures, et qu’un autre modèle d’IA a formalisé le résultat dans Lean après 17 heures supplémentaires. Les agents ont échangé près de 5 millions de messages, et Sébastien Bubeck, d’OpenAI, a estimé le coût de calcul à plusieurs millions de dollars, selon Quanta.

MIT Technology Review rapporte qu’OpenAI affirme ne pas prévoir de revendiquer le prix de $1 million. Selon Wikipedia, le contre-exemple n’a pas encore été vérifié par des mathématiciens externes ni par le Clay Mathematics Institute.

Ce dernier point est important. Une formalisation dans Lean est un signal fort, mais elle n’est pas équivalente à l’acceptation par la communauté. Quanta note que les preuves formelles peuvent établir qu’un énoncé découle de règles à l’intérieur de l’assistant de preuve, tandis que les mathématiciens doivent encore vérifier que l’énoncé formalisé est logiquement équivalent à l’affirmation mathématique que l’on entendait démontrer.

Les équations différentielles décrivent des relations entre des quantités qui changent. En mécanique des fluides, les équations de Navier–Stokes combinent vitesse, pression, viscosité, forces externes et conservation de la masse. Elles sont assez simples à écrire en notation standard, mais leur comportement à long terme peut être extrêmement difficile à comprendre.

La difficulté centrale n’est pas de savoir si les ingénieurs peuvent simuler des fluides. Ils le font, constamment. La question est de savoir si les équations mathématiques idéalisées sont garanties de bien se comporter dans les conditions spécifiées par le problème du prix du millénaire.

Une singularité signifierait que les équations prédisent une rupture : une partie du fluide évolue vers un état mathématique impossible. Comme l’explique Quanta, cela n’implique pas un échec pratique immédiat dans l’ingénierie du monde réel, car les fluides réels sont constitués de molécules et d’atomes plutôt que de continus parfaitement lisses. Mais en tant que mathématiques, cela montrerait que les équations idéalisées ont un comportement plus surprenant que beaucoup ne l’anticipaient.

Le problème est aussi lié à la turbulence, l’un des phénomènes les plus difficiles de la physique. Wikipedia décrit la turbulence comme l’un des plus grands problèmes non résolus de la physique, malgré son importance en science et en ingénierie. Une preuve d’explosion ne « résoudrait » pas la turbulence au sens pratique, mais elle modifierait ce que les mathématiciens savent des équations qui la sous-tendent.

La controverse porte sur la relation entre le travail d’OpenAI et celui de Buckmaster et Alpöge.

Quanta rapporte que l’annonce d’OpenAI est arrivée environ 12 heures après que Buckmaster a annoncé des résultats avec Alpöge sur des problèmes étroitement liés. Leur travail utilisait divers modèles d’IA, dont des modèles OpenAI. MIT Technology Review rapporte que Buckmaster et Alpöge travaillaient depuis près d’un an sur le problème et que Buckmaster a publié une preuve montrant qu’une version simplifiée des équations de Navier–Stokes peut s’effondrer.

Le travail d’OpenAI comme celui de Buckmaster–Alpöge semblent s’appuyer sur une approche associée à Diego Córdoba et Luis Martínez-Zoroa. Quanta indique que les deux équipes se sont fortement appuyées sur les travaux de Córdoba et Martínez-Zoroa, qui ont développé une stratégie s’écartant des méthodes utilisées par la plupart des mathématiciens. MIT Technology Review cite Javier Gómez-Serrano, professeur de mathématiques à Brown University, selon qui cette approche faisait partie de celles considérées comme prometteuses pour le problème.

OpenAI a reconnu, selon MIT Technology Review, que l’équipe avait été incitée à poursuivre le problème après avoir entendu une rumeur au sujet des efforts de Buckmaster et Alpöge. Le différend porte sur la question de savoir si les modèles ou les employés d’OpenAI ont eu accès au travail de Buckmaster et Alpöge, s’y sont entraînés ou en ont autrement bénéficié.

MIT Technology Review rapporte que Buckmaster a publié un document décrivant des interactions avec des employés d’OpenAI. Selon le récit de Buckmaster, des employés d’OpenAI ont présenté deux possibilités. Buckmaster et Alpöge pouvaient publier leur travail et OpenAI publierait sa solution à Navier–Stokes le lendemain, ou Buckmaster pouvait travailler avec OpenAI sur un article Navier–Stokes excluant Alpöge de la liste des auteurs en raison de son affiliation à Anthropic. MIT Technology Review rapporte également qu’OpenAI a démenti que ses employés ou ses agents aient accédé aux transcriptions de Buckmaster et Alpöge.

Ce sont des accusations sérieuses, mais les éléments publics restent incomplets. La bonne posture consiste à distinguer l’affirmation mathématique du différend sur l’attribution. La preuve peut être correcte tout en laissant le processus éthiquement contesté. Ou la preuve peut échouer à l’examen tandis que les questions d’attribution demeurent importantes.

Lean est un assistant de preuve : un système permettant d’exprimer des énoncés mathématiques et de vérifier que chaque étape découle de règles formelles. Dans les mathématiques à forts enjeux, cela peut éliminer une grande catégorie d’erreurs. Cela peut aussi rendre les preuves générées par IA plus faciles à auditer, car la preuve n’est pas seulement de la prose ; c’est une logique formelle exécutable.

C’est pourquoi le composant Lean est important. Si la formalisation est solide et correspond à l’énoncé Navier–Stokes visé, le résultat devient beaucoup plus difficile à écarter comme une hallucination fluide. Pour les concepteurs d’IA, c’est la différence entre un modèle qui écrit un raisonnement plausible et un système qui produit des artefacts qu’un autre programme peut vérifier.

Mais Lean ne résout pas tous les problèmes de confiance. Il n’établit pas la priorité. Il ne révèle pas comment la preuve a été trouvée. Il n’explique pas si des données privées, des transcriptions ou des idées non publiées ont influencé la recherche. Et il ne remplace pas le rôle de la communauté mathématique dans l’interprétation de l’importance de la preuve.

Cette distinction devrait sembler familière aux personnes qui construisent des produits d’IA. Les sorties structurées, les tests, les evals et les vérifications formelles peuvent rendre les systèmes plus fiables, mais ils ne répondent pas à eux seuls aux questions de gouvernance. Si un agent d’IA peut appeler des outils, inspecter des logs, réutiliser un contexte privé ou se coordonner avec d’autres agents, le système a besoin de limites et de pistes d’audit autant que de capacités brutes.

C’est l’une des raisons pour lesquelles le travail multi-agent est un problème d’ingénierie, pas seulement une astuce de prompting. Que vous conceviez des agents de recherche ou des workflows métier, les questions pratiques sont similaires : quels agents peuvent voir quel contexte, quels outils peuvent-ils appeler, où les transferts ont-ils lieu et qu’est-ce qui est journalisé ? Ces choix de conception comptent dans les agents d’IA bien avant que les enjeux atteignent le niveau d’un prix du millénaire.

Le détail opérationnel le plus frappant est l’échelle. Quanta rapporte environ 10 000 agents, 88 heures de recherche, 17 heures supplémentaires pour la formalisation et près de 5 millions de messages entre agents. MIT Technology Review rapporte qu’OpenAI a indiqué que l’exécution avait coûté des millions de dollars.

Cette échelle n’est pas accessible à la plupart des groupes universitaires. Elle suggère un avenir possible où les progrès mathématiques de pointe dépendent de modèles internes, de budgets de calcul privés et d’infrastructures d’agents concentrés au sein de quelques entreprises d’IA.

MIT Technology Review présente cela comme un tournant pour les mathématiques : si de grands problèmes ouverts peuvent être attaqués par des essaims privés d’agents, les normes de la collaboration académique pourraient être mises sous tension. Les mathématiciens apprennent souvent des tentatives ratées, des résultats partiels et des fausses pistes. Si tout cela se déroule dans des systèmes privés et ne devient jamais public, le domaine pourrait obtenir des réponses sans le chemin partagé qui crée traditionnellement de nouveaux outils et sous-domaines.

Quanta cite le mathématicien de Princeton Charles Fefferman, auteur de la description officielle du problème par le Clay Institute, disant qu’il était ravi que le problème soit résolu et désignant Córdoba et Martínez-Zoroa comme les héros de l’histoire. Cette attribution est un correctif utile. Même si l’étape finale était automatisée, le goût de la recherche — choisir une direction prometteuse — provenait de travaux mathématiques humains construits sur des années.

Pour les builders, la leçon n’est pas « utilisez plus d’agents ». Elle est que les systèmes agentiques amplifient la qualité de l’espace de recherche qui leur est donné. De meilleurs modèles et des budgets plus importants aident, mais le cadrage du problème, la sélection du contexte, l’accès aux outils et les boucles de vérification déterminent toujours si le système explore un territoire utile ou brûle du compute.

Si vous routez du travail entre plusieurs modèles, le même principe s’applique à plus petite échelle. Utilisez le meilleur modèle pour la tâche, mais ne traitez pas le choix du modèle comme l’ensemble du système. Le workflow qui l’entoure — récupération, contraintes, vérifications, approbations et logs — est la source de la fiabilité. En d’autres termes, la capacité vient de tout le workflow, pas d’un choix fondé sur un classement.

La première chose à surveiller est la validation mathématique. Des mathématiciens externes et le Clay Mathematics Institute devront prendre le temps d’évaluer si la preuve est correcte, si la formalisation Lean correspond à l’affirmation visée et comment le résultat s’inscrit dans les travaux antérieurs.

La deuxième est l’attribution. Les récits publics d’OpenAI, de Buckmaster, d’Alpöge et de mathématiciens extérieurs ne forment pas encore un dossier établi. Les questions centrales sont factuelles : à quoi les agents ou employés d’OpenAI ont-ils eu accès, sur quoi se sont-ils entraînés, que savaient-ils et quand l’ont-ils su ?

La troisième est de savoir si cela devient un modèle. Si les laboratoires d’IA de pointe peuvent pointer d’immenses essaims d’agents vers des problèmes célèbres non résolus, d’autres annonces suivront. Certaines seront nettes. Certaines seront contestées. Certaines échoueront à l’examen. Les domaines concernés auront besoin de normes pour le crédit, la divulgation, le calcul privé et les revendications de priorité assistées par IA.

Pour les personnes qui construisent avec l’IA en dehors des mathématiques pures, le message est assez clair : la capacité se déplace vers les systèmes, pas vers les prompts isolés. Agents, outils, routage de modèles et vérification deviennent l’unité de travail. Les équipes qui gèrent bien la provenance et l’examen seront mieux placées que celles qui ne font que poursuivre des sorties plus volumineuses.

Nous continuerons à suivre l’histoire de la vérification et de l’attribution à mesure qu’elle se développe. Si vous voulez de l’actualité IA avec le contexte technique intact, vous pouvez vous abonner à la newsletter LIA.

• OpenAI affirme que des agents d’IA autonomes ont trouvé une singularité dans les équations de Navier–Stokes tridimensionnelles et produit une formalisation dans Lean.
• Le résultat n’a pas encore été vérifié par des mathématiciens externes ni accepté par le Clay Mathematics Institute.
• Une preuve Lean peut réduire de nombreuses erreurs de vérification de preuve, mais les examinateurs doivent encore confirmer que l’énoncé formel correspond à l’affirmation mathématique visée.
• L’annonce est mêlée à un différend d’attribution impliquant les travaux de Tristan Buckmaster, Levent Alpöge, Diego Córdoba et Luis Martínez-Zoroa.
• L’échelle rapportée de l’exécution met en lumière un écart de ressources entre les laboratoires d’IA de pointe et la plupart des groupes universitaires.
• Pour les builders d’IA, l’épisode montre que les agents ont besoin de provenance, de pistes d’audit, de boucles de vérification et de limites claires, pas seulement de plus de compute.

Cette section répond aux questions pratiques derrière la revendication d’OpenAI sur Navier–Stokes : les réponses ci-dessous couvrent l’annonce, le rôle de Lean et les parties qui nécessitent encore un examen indépendant. Elle distingue aussi les enjeux mathématiques du différend d’attribution autour du travail.

OpenAI affirme disposer d’une solution générée par IA, mais cette revendication nécessite encore un examen mathématique externe et une évaluation par le Clay Mathematics Institute.

Selon les articles cités, OpenAI affirme que ses agents ont trouvé une singularité dans les équations de Navier–Stokes tridimensionnelles et qu’un autre modèle a formalisé le résultat dans Lean.

Lean peut vérifier que chaque étape formelle découle de règles, ce qui rend la preuve plus difficile à écarter comme simple prose plausible. Les mathématiciens doivent encore vérifier que l’énoncé formalisé correspond à l’affirmation Navier–Stokes visée.

Le différend porte sur la question de savoir si le travail d’OpenAI a bénéficié des recherches assistées par IA de Tristan Buckmaster et Levent Alpöge sans crédit approprié. OpenAI a démenti que ses employés ou ses agents aient accédé à leurs transcriptions, selon MIT Technology Review.

Non. Une preuve d’explosion modifierait la compréhension mathématique des équations qui sous-tendent le mouvement des fluides, mais elle ne résoudrait pas directement la turbulence comme problème pratique d’ingénierie.