Le 8 septembre 2026, OpenAI publie une preuve qui montrerait qu'une solution des équations de Navier-Stokes peut devenir singulière en un temps fini. Le texte fait 166 pages. Une version est formalisée en Lean, un langage où l'ordinateur vérifie chaque pas. Douze heures plus tôt, Tristan Buckmaster, de l'université de New York, et Levent Alpöge, d'Anthropic, avaient rendu publics des résultats voisins. Navier-Stokes est l'un des sept problèmes du millénaire. La question de septembre n'est pas seulement « la machine a-t-elle trouvé ». C'est « qu'est-ce qu'une preuve que personne n'a encore lue en entier ».
Pour commencer : l'eau du robinet, et une explosion
Les équations de Navier-Stokes décrivent comment un fluide se déplace : l'eau dans un tuyau, l'air autour d'une aile, la météo à grande échelle. On les utilise tous les jours dans les logiciels d'ingénierie. Le problème posé par l'institut Clay, avec un prix d'un million de dollars, est ailleurs. Il demande de prouver, pour la version la plus générale de ces équations en trois dimensions, que des solutions régulières existent et le restent, ou bien d'exhiber un cas où elles cessent de l'être.
« Cesser de l'être » a un sens précis. Une grandeur, par exemple une vitesse, devient infinie en un temps fini. Les mathématiciens parlent de singularité, ou de blow-up. Ce n'est pas une vague un peu forte. C'est un point où l'équation, telle qu'elle est écrite, ne décrit plus rien de physique. L'énoncé officiel est sur le site de l'institut Clay. Le lire évite de confondre « un logiciel calcule un écoulement » et « on a réglé la question théorique ».
💡 Lean vérifie la cohérence, pas l'énoncé
Une preuve formalisée en Lean est un texte que la machine refuse si un pas ne suit pas des axiomes. Elle dit que le raisonnement tient debout à l'intérieur du fichier. Elle ne dit pas que le fichier répond à la question posée par Clay, ni qu'un humain en a compris la stratégie. C'est la même distinction que dans un banc d'essai : le test vert dit que le test est vert.
Deux annonces, et ce que chacune revendique
Le billet d'OpenAI du 8 septembre présente le travail comme une solution au problème d'existence et de régularité, produite par un système interne. Le billet dit que la dynamique peut développer une singularité en temps fini, et que l'entreprise publie à la fois une rédaction et une formalisation Lean.
Sur la course, le même billet est précis. L'effort aurait commencé le 1er septembre, après une rumeur que l'entreprise a ensuite rattachée à Alpöge et à Buckmaster. OpenAI écrit avoir proposé une publication simultanée et la reconnaissance de l'antériorité de l'autre équipe. Elle écrit aussi que ni ses chercheurs ni ses agents n'ont vu le travail de l'autre équipe avant la publication publique, et qu'une enquête interne a conclu que les prompts Codex de Buckmaster, dans les deux mois précédents, n'ont pas pu influencer le système, y compris par l'entraînement. Le modèle interne est décrit comme issu d'un apprentissage par renforcement à grande échelle, posé sur un modèle déjà préentraîné.
Le billet distingue les résultats. Sur les équations d'Euler, proches de Navier-Stokes sans la viscosité, Alpöge et Buckmaster auraient prouvé un résultat avec un forçage extérieur, et le système d'OpenAI un résultat sans ce forçage. Les preuves « diffèrent significativement », dit l'entreprise.
New Scientist, le jour même, donne d'autres chiffres, attribués à la conférence de presse : environ 10 000 agents, 50 heures pour trouver des blow-ups dans un cas, puis 11 heures pour étendre, et un coût d'environ 15 millions de dollars si un client voulait relancer le même problème. Ce 15 millions est un ordre de grandeur annoncé par l'entreprise, pas une facture d'un client. Buckmaster et Alpöge, dans le même article, disent avoir reçu « une aide considérable » de grands modèles, y compris ceux d'OpenAI, et avoir publié des résultats considérés comme des étapes vers le problème, pas la clôture du prix.
The Verge, le 12 septembre, rapporte l'autre version de la négociation. Buckmaster dit que les échanges avec Sébastien Bubeck, chez OpenAI, sont devenus conflictuels. Il dit s'être vu offrir, en substance, un accès au calcul et la signature unique du papier d'OpenAI, à condition d'écarter Alpöge. Il appelle cela un pot-de-vin et dit avoir refusé. Il s'interroge aussi sur ce que ses usages de Codex ont pu apprendre à l'entreprise. OpenAI, de son côté, maintient que les prompts n'ont pas alimenté le système. Nous n'arbitrons pas. Les deux récits sont publics, ils ne décrivent pas la même conversation, et aucun des deux n'est une relecture des 166 pages.
Ce que mi-octobre a ajouté
Le 13 octobre, Scientific American titre que la preuve-choc n'est pas celle qu'on avait crue. L'article, dans ce que nous en avons lu, retient trois faits. La rédaction fait 166 pages. Les premiers récits, y compris ceux de l'entreprise, présentaient la preuve comme suivant le programme des mathématiciens madrilènes Diego Córdoba et Luis Martínez-Zoroa. Un essaim d'environ 10 000 copies du modèle aurait passé quelque 88 heures et 130 milliards de jetons à construire un blow-up. Le magazine écrit que les mathématiciens sont en train de comprendre un événement plus étrange que l'annonce du 8 septembre.
Nous n'allons pas plus loin que cette phrase. Trancher si la version démontrée est celle du prix Clay, si le forçage a été réintroduit, si la stratégie est bien celle de Madrid : c'est le travail des gens qui lisent les 166 pages. Au 14 octobre, cette lecture collective n'est pas terminée. L'institut Clay n'a pas, dans les sources que nous avons ouvertes, déclaré le problème résolu.
La part de l'IA, elle, se décrit sans attendre ce verdict. Des agents ont cherché, rédigé et formalisé. La stratégie d'attaque vient d'un programme mathématique humain, que deux équipes disent avoir suivi. La formalisation dit que des pas s'enchaînent. Elle ne distribue pas le crédit, et elle ne remplace pas la revue par les pairs.
Ce que la course change pour les chercheurs
Le point qui reste, même si la preuve est un jour acceptée, même si elle est un jour réduite à une étape, est celui-ci. Travailler un problème ouvert dans un outil hébergé par une entreprise qui poursuit le même problème expose les idées inachevées. Buckmaster pose la question. OpenAI répond qu'une enquête a écarté l'influence des prompts. Les deux phrases peuvent être vraies ensemble : une enquête interne peut ne rien trouver, et un chercheur peut quand même juger le risque trop haut pour continuer à taper ses brouillons au même endroit.
C'est le sujet, vu du côté de l'utilisateur, de ce que deviennent les conversations. Un brouillon mathématique n'est pas une confidence intime. C'est quand même un travail non publié. Le geste de prudence est le même : ne pas coller dans la fenêtre ce qu'on n'est pas prêt à voir ressortir ailleurs.
L'argent du calcul, des millions de dollars pour quelques jours d'agents, replace aussi l'épisode dans l'économie de l'IA en 2026. Un laboratoire qui peut lancer 10 000 agents n'est pas un département de mathématiques. La vitesse obtenue est réelle dans les récits des deux camps. Elle a un prix d'entrée que la plupart des équipes n'ont pas.
Le fil avec Dartmouth est plus calme qu'il n'y paraît. En 1956, une conférence a été retenue pour des promesses, alors que peu de programmes tournaient. Nous l'avons raconté dans le mythe fondateur de Dartmouth. Septembre 2026 inverse la proportion : il y a un artefact énorme, une formalisation, des dépôts, et le sens de l'artefact n'est pas encore stabilisé. C'est un progrès de méthode. Ce n'est pas encore une ligne dans la liste des problèmes résolus.
