Ce qu’OpenAI a mis en ligne
OpenAI a publié les éléments qui sous-tendent son affirmation d’avoir trouvé une singularité en temps fini dans les équations de Navier-Stokes en trois dimensions : un compte rendu sur son propre site, un article et des fichiers de preuve vérifiables par machine dans un dépôt GitHub public. L’entreprise indique qu’elle n’a pas l’intention de réclamer le prix d’un million de dollars du Clay Mathematics Institute.
C’est le changement par rapport à lundi, où l’affirmation n’existait que sous la forme d’une description circulant entre chercheurs. Le dépôt contient des formalisations en Lean 4, construites sur Mathlib et publiées sous licence Apache 2.0, pour deux cas de Navier-Stokes à viscosité positive — l’un dans l’espace entier, l’autre sur le tore périodique — ainsi qu’une construction d’Euler associée. Quiconque dispose de Lean peut désormais exécuter le certificat plutôt que de croire sur parole.
Les chiffres avancés par OpenAI
Les chiffres de calcul proviennent d’OpenAI et n’ont pas été audités de façon indépendante. L’entreprise dit avoir utilisé un modèle interne qu’elle décrit comme nettement plus performant que GPT-6 Astra, et qu’environ 10 000 agents ont fonctionné en parallèle pendant près de 88 heures début septembre, produisant de l’ordre de 130 milliards de jetons de sortie. Environ 17 heures supplémentaires, selon The Next Web, ont servi à formaliser l’argument avec GPT-6 Astra.
Ce sont des moyens, pas des preuves. La preuve, c’est le fichier Lean, et Lean se moque du nombre d’agents qui l’ont écrit.
Pourquoi le prix n’est pas réclamé
La formulation de Clay du problème de Navier-Stokes se décompose en quatre énoncés. OpenAI affirme que son résultat établit les énoncés C et D : les alternatives de rupture, qui résolvent le problème en exhibant une solution qui cesse d’être régulière. L’entreprise dit aussi qu’elle ne réclamera pas le prix.
La raison tient à la construction. Le fluide part du repos et une force extérieure régulière lui est appliquée en permanence, et la singularité apparaît sous cette force. Savoir si un exemple forcé compte pour la question classique relève du jugement des mathématiciens et de Clay, pas d’un assistant de preuve. La page de l’institut continue de classer Navier-Stokes parmi les problèmes ouverts.
La querelle de paternité continue
Le résultat arrive au milieu d’une dispute qu’Aivio News a racontée lundi. Tristan Buckmaster, de l’université de New York, et Levent Alpöge, d’Anthropic, ont mis en ligne leurs propres preuves d’explosion assistées par IA et vérifiées en Lean pour les équations du milieu poreux, de Boussinesq et d’Euler, et Buckmaster a publié une déclaration décrivant la manière dont OpenAI l’a approché au sujet du calendrier et de la paternité du résultat sur Navier-Stokes. Sébastien Bubeck, d’OpenAI, a qualifié ce récit de faux et d’incendiaire.
Quanta Magazine rapporte que Charles Fefferman, de Princeton, auteur de l’énoncé officiel du problème, a désigné Diego Córdoba et Luis Martínez-Zoroa comme les héros de l’histoire : le duo dont la méthode non calculatoire sert de socle aux deux travaux.
Ce qu’il faut surveiller
Deux choses sont désormais vérifiables plutôt que discutables. La première : des mathématiciens indépendants vont-ils compiler les fichiers Lean et confirmer qu’ils démontrent ce que dit le compte rendu. La seconde : le Clay Mathematics Institute se prononcera-t-il sur les termes de forçage. D’ici là, la description honnête est qu’une singularité vérifiée par machine existe et que son rapport à la question du prix reste indécis.
