Navier-Stokes, la preuve d’OpenAI attend toujours ses relecteurs

Le fait

Concrètement, la preuve décrit un fluide au départ lisse et au repos, auquel on applique une force lisse, et dont l’énergie reste finie sur toute la dynamique. Au bout d’un temps fini, une grandeur physique part à l’infini. C’est ce qu’on appelle une singularité : les équations cessent de décrire quoi que ce soit.

Le calendrier tient en une semaine. Le modèle interne est entraîné à partir du 28 août. Les agents sont lancés le 1er septembre. Ils parviennent à la résolution le samedi 5 septembre, soit 88 heures plus tard. La formalisation dans l’assistant de preuve Lean prend 17 heures de plus et s’achève le 6 septembre, exécutée par GPT-6 Astra. Une centaine d’agents avaient auparavant passé une cinquantaine d’heures sur un problème d’échauffement, les équations d’Euler.

Les volumes annoncés donnent la mesure du dispositif. Tous problèmes confondus, les agents ont échangé 4,9 millions de messages. Sur les 300 milliards de tokens de sortie produits par les agents d’OpenAI, 130 milliards ont servi au seul problème de Navier-Stokes, soit 43 % de l’effort annoncé le 8 septembre 2026. En messages, la concentration est encore plus nette : 2,7 millions sur 4,9, soit 55 %. Un agent, ici, est une instance du modèle qui travaille en parallèle des autres et dialogue avec elles : les mêmes essaims ont déposé 17 000 éditions sur un wiki allemand en six semaines.

Un point technique décide de beaucoup dans cette affaire : le résultat porte sur le cas avec forçage, c’est-à-dire avec une force extérieure lisse appliquée au fluide. C’est bien l’une des options de l’énoncé officiel rédigé par Charles Fefferman pour le Clay Institute, les options c et d, comme le rappelle le mathématicien qui conteste aujourd’hui le récit d’OpenAI.

Notre regard

La preuve existe ; la vérification, elle, pose une question. Un certificat Lean qui compile est un objet solide, puisque la machine rejoue chaque étape logique. Mais ce certificat a été produit par un modèle de la maison qui annonce le résultat, et le texte de la preuve, une centaine de pages, n’avait été lu par aucun mathématicien extérieur au moment de l’annonce.

OpenAI écrit ne pas avoir l’intention de réclamer le million de dollars attaché au problème. C’est aussi la seule position tenable. Le règlement du Clay exige une publication dans un support qualifiant, puis au moins deux ans écoulés depuis cette publication, puis une acceptation générale par la communauté mathématique mondiale. Aucun prix ne peut donc tomber avant septembre 2028, et encore, à condition que la publication ait lieu et tienne.

Le raccourci « une IA vient de gagner un million de dollars » ne tient donc pas.

La nuance

Le 8 septembre également, Tristan Buckmaster (Courant Institute, université de New York) et Levent Alpöge ont rendu publics trois résultats d’explosion en temps fini avec forçage lisse : milieux poreux incompressibles, Boussinesq, et Euler incompressible en dimension 3. Dans sa déclaration publique, Buckmaster date ces résultats du 15 août et leur vérification Lean du 22 août, et attribue l’idée du programme à Diego Córdoba et Luis Martínez-Zoroa, ce dernier méritant selon lui « une médaille Fields ».

Il raconte ensuite deux appels du dimanche 6 septembre avec des responsables d’OpenAI, dont Sébastien Bubeck. On lui aurait présenté un modèle interne à qui l’énoncé aurait simplement été donné, avec « très peu d’intervention humaine ». « Cela s’est révélé faux », écrit-il : une équipe entière travaillait sur le problème, le modèle avait d’abord été lancé sur des questions plus faciles dont Euler, et le prompt qu’on lui montrait avait lui-même été écrit en passant par Codex. Il rapporte qu’il a fini par être admis que le premier prompt datait « de ces derniers jours, après que l’information sur notre travail était parvenue à OpenAI ». Sur l’entraînement, sa phrase est nette : « On m’a dit que le modèle ne consultait pas les données utilisateurs. J’ai reposé la question, à propos de l’entraînement, et je n’ai pas obtenu de réponse. »

Buckmaster borne lui-même sa charge : « Je n’ai pas vu la preuve d’OpenAI. Je ne sais pas ce que leur modèle a fait, ni comment. Je ne sais pas si nos données ont été utilisées. Je n’accuse personne de rien. » OpenAI, de son côté, affirme n’avoir rien vu de ce travail avant sa publication, dit avoir proposé une sortie simultanée et une reconnaissance de leur priorité, et concède une réserve : « Bien que ce soit peu probable, nous ne pouvons pas exclure que des données dépersonnalisées issues de leur usage de nos produits aient contribué à améliorer nos modèles. »

Les deux chronologies se répondent jour par jour.

À surveiller

Trois échéances. La lecture de la preuve par des mathématiciens extérieurs d’abord : cent pages, aucune validation indépendante à ce stade. Le calendrier du Clay ensuite, qui ne commence à courir qu’à partir d’une publication qui n’a pas encore eu lieu. Une inquiétude plus large enfin, formulée par Terence Tao.

Le soir du 8 septembre, Terence Tao écrit sur Mathstodon que la réserve de bons problèmes ouverts est désormais exploitée « de façon non renouvelable », au risque de devenir rare. Son analogie : une région peut manquer d’eau potable tout en étant entourée d’un océan. On fabrique des problèmes ouverts à volonté, mais l’immense majorité n’apprend rien à personne.

Six des sept problèmes du millénaire restent ouverts ; seule la conjecture de Poincaré a été démontrée, par Grigori Perelman. Et reste la phrase par laquelle Buckmaster referme sa déclaration : si un modèle d’OpenAI a bien comblé l’écart jusqu’à Navier-Stokes, c’est une chose remarquable, et elle doit être dite haut et fort, par eux, « avec l’histoire intacte ».