OpenAI, soucieuse de démontrer l'intelligence de son modèle Astra, a mis en ligne le 8 septembre 2026 une démonstration qui, selon l’entreprise, résout le problème du millénaire de Navier-Stokes, réputé insurmontable. Le résultat provient d’un système d’agents utilisant un modèle interne. Il est accompagné d’un texte mathématique et d’une formalisation en Lean. L’annonce porte sur une possibilité précise : un écoulement initialement régulier peut développer une singularité en un temps fini. Elle met aussi en lumière une organisation de la recherche associant exploration parallèle, réorientation humaine et vérification formelle.
Une singularité avec une énergie qui reste bornée
Le document de 166 pages décrit un fluide incompressible en trois dimensions, initialement au repos, soumis à une force extérieure lisse. À l’approche d’un instant fini, sa vitesse devient non bornée alors que son énergie cinétique reste bornée. La construction revendiquée conserve une viscosité positive, cette propriété qui tend à dissiper les mouvements. Le contraste entre divergence locale de la vitesse et énergie totale finie est au cœur du résultat.
Les auteurs construisent un vortex dont le cœur se contracte en devenant de plus en plus fin. La région où les vitesses deviennent extrêmes se resserre suffisamment pour que l’énergie reste limitée. Le travail technique consiste notamment à faire se compenser les termes des équations afin que la force appliquée demeure régulière. Il s’agit d’établir l’existence d’une configuration répondant à ces conditions, sans affirmer que tous les écoulements finissent par se comporter ainsi.
Le recours à une force extérieure est expressément prévu dans les options C et D de l’énoncé officiel du Clay Mathematics Institute. Une démonstration conforme à l’une de ces options répondrait donc bien au problème posé. Sa portée reste circonscrite : une singularité construite avec forçage ne tranche pas, par elle-même, le cas sans force extérieure.
La recherche répartie entre des milliers d’agents
OpenAI décrit un groupe d’environ 10 000 agents simultanés, arrivé au résultat 88 heures après le lancement des premiers agents, avec ensuite 17 heures supplémentaires de formalisation et de vérification avec GPT-6 Astra. Les chercheurs ont réparti les approches, réaffecté des ressources après une avancée sur les équations d’Euler et fait circuler les résultats intermédiaires entre groupes. Le dispositif associe donc calcul massif et choix d’organisation.
Le volume annoncé pour Navier-Stokes atteint environ 130 milliards de tokens de sortie. Aucun montant financier n’accompagne ce chiffre. Les durées et le nombre d’agents décrivent une expérience de recherche ; ils ne permettent pas de calculer le prix d’une découverte ni le gain de productivité d’un laboratoire ordinaire. La qualité des pistes transmises entre groupes et les critères utilisés pour réorienter l’effort comptent aussi dans l’interprétation de cette performance.
Lean rend la démonstration contrôlable
Le dépôt public fournit les fichiers de formalisation et des instructions de vérification. Il contient aussi un énoncé de comparaison adapté du projet Formal Conjectures de Google DeepMind. Cette séparation aide à contrôler que le théorème démontré correspond à la cible annoncée, un enjeu différent de la seule production d’un raisonnement convaincant en langage naturel.
L’outil Comparator vérifie notamment la correspondance entre l’énoncé de référence et la solution, les axiomes autorisés et l’acceptation de la preuve par le noyau Lean. L’intérêt scientifique est de mettre à disposition un objet que d’autres équipes peuvent examiner. Il reste nécessaire de comprendre les définitions choisies et leur correspondance avec le problème mathématique ; une vérification formelle annoncée ne dispense pas de ce travail.
Cette chaîne peut modifier la façon d’évaluer une contribution de l’IA à la recherche. L’examen peut porter sur les énoncés et les objets produits, au-delà du récit de performance du fournisseur. La compréhension des idées nouvelles reste tout aussi utile : elle détermine si les méthodes pourront être reprises, simplifiées ou étendues à d’autres problèmes.
La reconnaissance d’une solution suit enfin son propre calendrier. Les règles du prix Clay prévoient notamment une publication qualifiée, au moins deux ans d’attente après celle-ci et une acceptation générale par la communauté mathématique. OpenAI indique ne pas vouloir réclamer le prix. À ce stade, l’événement est la mise à disposition d’une preuve revendiquée et de ses éléments de contrôle, dont l’examen scientifique peut commencer.