Théorème de Navier-Stokes : les Big Tech entre comprendre, vérifier et ralentir

J'ai attendu quelques semaines que la poussière de la polémique et du battage médiatique (hype) se retombe, avant de tenter de raconter ce qui s'est réellement passé avec Navier-Stokes. Les premiers jours, les titres se sont divisés en deux camps opposés : « L'intelligence artificielle a résolu un problème du millénaire » d'un côté, « Non, ils ont seulement volé le travail de deux mathématiciens » de l'autre. Tous deux reflètent le ton de l'affaire, non les faits. Et les faits, mis bout à bout, dessinent une histoire bien plus intéressante que n'importe quel titre. Il y a ensuite un fil qui relie cette histoire à une autre arrivée quelques jours plus tard, l'essai dans lequel Dario Amodei a demandé de ralentir le développement de l'IA : la même question sur ce qui est vérifiable dans ces récits d'entreprise et ce qui reste une simple promesse. Nous y viendrons après les mathématiques.
Une machine, un fichier et un doute qui demeure
Le 8 septembre, OpenAI a publié ce qu'elle définit comme une solution generée par un modèle interne à l'une des questions ouvertes les plus célèbres des mathématiques : les équations de Navier-Stokes peuvent-elles, dans certaines conditions, « exploser » ? La réponse arrive sous deux formes : un document de plus de 160 pages et un fichier vérifié par le logiciel Lean, qui contrôle chaque étape logique comme le ferait un correcteur implacable, sans jamais se fatiguer et sans jamais se distraire.
Dans le même temps, cependant, certains des mathématiciens les plus autorisés au monde affirment que la pièce la plus importante — comprendre vraiment ce qui se passe à l'intérieur de ces équations — n'est pas encore arrivée. Terence Tao, médaille Fields et probablement le mathématicien vivant le plus suivi en ligne, l'avait écrit cinq jours avant que la solution ne soit rendue publique, et avant même de savoir qu'elle existait. Ce n'est pas une réaction, c'est une prédiction qui s'est réalisée. Tao craignait un scénario dans lequel une solution « en grande partie générée par l'IA » finirait par contaminer le problème comme source de progrès ultérieurs, au lieu de le faire avancer.
Cet article tente de tenir ensemble les deux aspects sans choisir de camp : ce qui a été effectivement vérifié, ce qui reste de la narration, et quelles questions restent ouvertes.
De quoi parlons-nous
Les équations de Navier-Stokes sont, au fond, la deuxième loi de Newton appliquée aux fluides. Elles décrivent comment se déplacent l'eau, l'air, le sang dans les artères, l'atmosphère. Elles sont utilisées chaque jour pour concevoir des avions, prédire la météo, étudier la circulation sanguine. Le problème mathématique qui les concerne n'a cependant rien à voir avec la météorologie de demain : la question est de savoir si un fluide qui part d'un état calme et régulier, avec une énergie limitée, peut rester régulier pour toujours, ou si à un moment donné peut apparaître un point où la vitesse croît sans limite, en un temps fini. Imaginez une goutte à l'intérieur d'un tourbillon qui se resserre de plus en plus, jusqu'à un point de dimension zéro qui tourne à une vitesse infinie : c'est ce que les mathématiciens appellent un « blowup » (explosion/effondrement), et c'est précisément ce qui, selon la physique réelle, ne devrait jamais se produire, car le frottement interne du fluide tend toujours à lisser le mouvement.
En deux dimensions, on sait depuis longtemps que cela ne se produit jamais. En trois dimensions, la question reste ouverte depuis près de quatre-vingt-dix ans, depuis le travail pionnier de Jean Leray en 1934, et a été inscrite en 2000 parmi les sept problèmes du prix du millénaire du Clay Mathematics Institute, chacun doté d'un prix d'un million de dollars. La seule fois où le prix a été attribué, c'était en 2010 pour la conjecture de Poincaré, et le vainqueur, Grigori Perelman, l'a refusé.
OpenAI revendique le côté « explosion » : une configuration dans laquelle, avec une force externe lisse appliquée au fluide et une énergie restant finie tout au long de la dynamique, une singularité se développe tout de même en temps fini. La difficulté technique n'est pas décorative : l'effondrement doit naître du mouvement propre du fluide, et non de quelque chose d'artificiel introduit de force.
Pourquoi cela importe-t-il à quelqu'un, si cela ne change pas la façon dont nous prédisons la météo demain ? Parce que, comme l'écrit Tao, le problème n'est pas important pour son application physique directe, mais pour ce qu'il génère en chemin : des décennies de tentatives de réponse ont produit des outils mathématiques aujourd'hui fondamentaux, des solutions faibles de Leray-Hopf aux critères d'effondrement de Beale-Kato-Majda. Le problème a toujours été, en d'autres termes, un générateur de théorèmes, et non un prix à encaisser.

Lean vérifie la logique, pas la question
La partie la plus mal comprise de toute cette affaire concerne précisément ce fichier vérifié dans Lean. Lean est un assistant de preuve, un programme né chez Microsoft en 2013 qui vérifie pas à pas si chaque déduction découle correctement des précédentes. C'est la raison pour laquelle l'annonce semble plus solide qu'un simple communiqué de presse : la preuve n'est pas l'opinion d'un modèle linguistique, c'est un fichier qu'une machine vérifie mécaniquement.
Le problème est que Lean vérifie si la démonstration découle de l'énoncé écrit, non si l'énoncé écrit est le bon. Si la traduction du problème en langage formalisé — ce que signifient exactement « solution », « énergie finie », « lissé » — est imprécise, la preuve peut être impeccable sans démontrer du tout ce que l'on croit qu'elle démontre. Lance Fortnow, théoricien de la complexité, note également un effet secondaire : Lean devient une sorte de tampon postal, un moyen de revendiquer la priorité sur un théorème avant même de l'avoir écrit de façon compréhensible pour les humains. Il raconte que quelques jours plus tôt, Anthropic avait formalisé dans Lean l'intégralité du dernier théorème de Fermat, et que la nouvelle « avait à peine fait du bruit » : signe que le genre se sature.
C'est sur ce point qu'intervient la contribution la plus utile apparue après la première vague de titres, un texte de Silvia De Toffoli et Eamon Duede publié en tant qu'invités sur le blog de Tao. Leur thèse est qu'il existe deux notions distinctes de preuve : la preuve logique, la validité déductive contrôlable mécaniquement, qu'une formalisation Lean satisfait pleinement et qui garantit la certitude ; et la preuve intelligible, qui concerne la compréhension, le fait de comprendre pourquoi quelque chose est vrai. Historiquement, les deux ont toujours marché ensemble, car aucun humain ne pouvait construire une preuve logique colossale sans d'abord saisir les idées qui la rendaient vraie. Avec l'IA, écrivent-ils, ces deux notions peuvent désormais se séparer de manière dramatique. La phrase qui résume le mieux toute la question est la leur : OpenAI a donné une réponse, mais il est loin d'être clair qu'elle ait offert une solution féconde. Et ce n'est pas une opinion isolée : le Clay Institute lui-même écrit, sur la page officielle du problème, qu'une démonstration compte parce qu'elle apporte non seulement la certitude, mais aussi la compréhension. C'est la règle écrite du concours, mise en crise par le concours lui-même.
Dix mille tentatives et une voie déjà tracée
La partie la plus intéressante de l'affaire est cependant la manière dont on parvient à un tel résultat, car elle en dit plus que n'importe quelle déclaration sur ce que la machine a effectivement accompli. Selon la reconstitution d'OpenAI, l'entreprise a mis au travail environ dix mille agents concurrents, divisés en groupes explorant des approches différentes : certains cherchaient la preuve que le fluide explose, d'autres la réfutation opposée, sans qu'il soit demandé au système laquelle des deux était vraie. Le coût computationnel global, estimé par Simon Willison sur les trois cents milliards de tokens utilisés pour tous les problèmes ouverts tentés durant ces jours-là (et non sur les seuls cent trente milliards dédiés à Navier-Stokes), tournerait autour de quinze millions de dollars aux tarifs officiels.
Pourtant, le chemin que dix mille agents ont parcouru en quatre-vingt-huit heures n'a pas été ouvert par une machine ; il a été tracé par deux mathématiciens humains des années auparavant. Diego Córdoba et Luis Martínez-Zoroa exploraient depuis 2023 la construction d'effondrements forcés pour des équations apparentées. Leur travail a permis à Tristan Buckmaster, professeur à l'Université de New York, et Levent Alpöge, chercheur travaillant également pour Anthropic, d'obtenir des résultats analogues pour d'autres équations au cours d'une année de collaboration personnelle financée de leur propre poche. Córdoba le dit avec une phrase qui vaut plus que n'importe quelle analyse technique : si leur travail n'avait pas existé, l'intelligence artificielle n'aurait pas résolu le problème. Et Tao lui-même, le 3 septembre, trois jours avant l'annonce, avait déjà décrit publiquement la stratégie en quatre étapes menant à la solution, la qualifiant de « stratégie raisonnablement bien définie ». La machine n'a pas trouvé la voie : elle l'a parcourue en quatre-vingt-huit heures au lieu de mois.
Cela ne signifie pas qu'il s'agisse de pure force brute. Bryna Kra, mathématicienne spécialisée dans un autre problème de longue date, la conjecture de Nivat, raconte qu'elle et ses collègues ont pressenti pendant des années où se cachait le lien entre deux approches différentes, sans parvenir à le trouver. Une machine, écrit-elle, n'a pas besoin d'années pour absorber des domaines distincts des mathématiques avant de trouver des connexions, et peut tester des milliers de combinaisons sans jamais se décourager. C'est un compliment, pas une condamnation : la machine réussit bien la partie mécanisable, chercher, combiner, vérifier sur une carte déjà dessinée par d'autres. Elle n'a pas encore montré qu'elle savait générer la question suivante, celle qui décide où creuser la prochaine fois.
Il y a cependant un revers plus inquiétant à tout cela, et c'est peut-être la thèse la plus forte avancée par Tao dans cette affaire. Si un processus itératif de ce type — qui génère normalement des intuitions précieuses sur le fonctionnement réel des fluides — est mené entièrement par une entreprise qui garde le parcours presque totalement hors de la vue du public, alors même en résolvant techniquement le problème, on n'ajoute presque rien au savoir collectif. La véritable ligne de partage, selon cette lecture, n'est pas force brute contre ingéniosité humaine, c'est processus publié contre processus caché. OpenAI a rendu publique la destination, pas le chemin.

Vingt-cinq médailles Fields, une préoccupation partagée
Le 11 septembre, vingt-cinq médaillés Fields, dont Tao lui-même, ont signé une déclaration rédigée à la hâte, sans le processus de consultation habituel, « parce que l'urgence de la situation » l'exigeait. Le texte ne condamne pas l'usage de l'intelligence artificielle en soi, mais dénonce un désalignement entre les objectifs des entreprises développant ces modèles et ceux de la communauté mathématique : résoudre des problèmes pour servir de vitrine publicitaire risque d'endommager la discipline elle-même. La production de plus en plus rapide d'énoncés vrai-faux, écrivent-ils, pourrait détruire un terrain fertile au lieu de donner naissance à de nouvelles idées, et la précipitation avec laquelle ces résultats sont annoncés soulève également de sérieuses inquiétudes quant à l'attribution du mérite.
La European Mathematical Society, dans un communiqué du 10 septembre signé par son président Jan Philip Solovej, arrive à une formule qui constitue peut-être la critique la plus percutante : il ne suffit pas de dire que l'IA ne sait pas faire de mathématiques, le vrai problème est que le modèle utilisé pour ce résultat reste interne à OpenAI et n'est accessible à personne d'autre. Dans un esprit de science ouverte, écrit l'EMS, c'est un problème que la communauté mathématique doit affronter. Ce n'est pas une objection sur le fond du résultat, c'est une objection sur l'accès.
Le crédit contesté
L'aspect le plus délicat concerne ce qui s'est passé exactement entre le 3 et le 8 septembre, et ici la règle veut que ce qui est contesté soit attribué à ceux qui l'affirment, sans prendre parti. Buckmaster raconte, dans un document publié quelques heures avant l'annonce officielle, avoir été contacté par OpenAI après avoir écrit lui-même à un chercheur de l'entreprise, inquiet que les rumeurs sur son travail avec Alpöge n'aient déclenché une course concurrente. Lors d'un appel le 6 septembre, on lui décrit une preuve pour un Navier-Stokes « forcé », précisément la direction que lui et Alpöge avaient choisie discrètement : il qualifie cela de signal d'alarme, car ce n'est pas une direction à laquelle on arrive en quelques jours en partant uniquement de l'énoncé du problème. Buckmaster raconte aussi s'être entendu dire, à propos de la possibilité de rester à l'écart de la publication, la phrase « pourquoi gâcher ta carrière ? », qu'il a vécue comme une menace voilée.
Sébastien Bubeck, chercheur chez OpenAI présent lors de cet appel, a publié une version différente du même épisode : il affirme avoir fait cette remarque dans un contexte complètement différent, en débattant de qui devait figurer comme premier auteur lors d'une réécriture de la preuve par OpenAI, et s'être excusé sur-le-champ pour le choix de mots malheureux. Sam Altman, de son côté, a écrit que son équipe avait agi avec intégrité, qu'ils croyaient initialement travailler en vue d'une annonce conjointe, et qu'après avoir découvert que Buckmaster et Alpöge avaient résolu un problème différent (Euler, non Navier-Stokes), ils leur avaient proposé de publier en premier. Alpöge, sur son propre profil, confirme les faits principaux mais attribue une signification opposée aux mêmes événements, revendiquant explicitement avoir toujours utilisé et souhaité remercier publiquement les outils d'IA, y compris ceux d'OpenAI, dans son travail.
Les deux versions de ce coup de téléphone restent incompatibles, et il n'y a pas d'éléments permettant d'établir laquelle est exacte. Ce qui est en revanche vérifiable, selon un contrôle d'Emily Riehl sur X diffusé le 9 septembre 2026, c'est la bibliographie : des vérifications sur la Wayback Machine confirment que le document public d'OpenAI a été mis à jour le 8 septembre à 19h09 GMT, en ajoutant précisément les références à Córdoba et Martínez-Zoroa qui manquaient dans la première version. Ce n'est pas une opinion, c'est une horodatage.
Le paradoxe du « ralentissement »
Un détail relie cette affaire à un événement presque parallèle survenu quelques jours plus tard. Le 12 septembre, Dario Amodei, président-directeur général d'Anthropic, publiait un essai intitulé We Must Pace the Frontier (« Nous devons réguler le rythme de la frontière »), dans lequel il soutient que l'industrie doit délibérément ralentir le rythme auquel elle augmente les capacités de ses modèles. En quelques heures, Sam Altman écrivait être d'accord, et Elon Musk répondait par deux mots : « Dario is right » (Dario a raison). C'est le même terme exact, pacing (cadencement/régulation du rythme), qui apparaît quatre jours plus tôt sur la page d'OpenAI consacrée au résultat Navier-Stokes, où l'entreprise écrit vouloir guider et cadencer le rythme de ses progrès.
Ce n'est pas un détail décoratif. Amodei lui-même explique que la marge dont disposent les entreprises américaines pour ralentir dépend de l'avance qu'elles possèdent par rapport à la Chine, et consacre une part importante du texte à demander au gouvernement de bloquer la vente de puces avancées à Pékin et de lutter contre la distillation de modèles — la pratique consistant à entraîner un modèle plus petit pour imiter un modèle plus puissant. Si ces mesures sont bien exécutées, écrit-il, elles élargiraient l'avantage américain au cours des trois à cinq prochaines années.
Les lectures critiques ne se sont pas fait attendre et émanent de milieux très divers. The Register l'a décrite comme une tentative d'obtenir des conditions réglementaires favorables sous le masque d'un appel à la sécurité. Une analyse indépendante note que l'essai demande deux choses très concrètes au gouvernement — stopper la vente de puces à la Chine et contrer la distillation —, tandis que la partie sur la coopération internationale servirait plutôt à construire une image de responsabilité qu'à produire un accord réaliste avec Pékin, qu'Amodei lui-même, selon cette lecture, sait irréalisable. Même les observateurs prudents du secteur remarquent qu'un engagement réel à ralentir signifierait arrêter les entraînements, pas seulement ajouter des observateurs externes disposant d'un droit de publication : les observateurs peuvent être ignorés, les entraînements non. Même un commentaire de la presse d'État chinoise, qui a évidemment son propre intérêt à le souligner, arrive à la même conclusion, lisant l'essai comme un outil pour préserver l'hégémonie technologique américaine plutôt que comme une proposition de sécurité partagée.
Tout le monde ne lit pas l'essai comme un simple exercice de communication. Demis Hassabis, président-directeur général de Google DeepMind, l'a qualifié publiquement de pas dans la bonne direction, ajoutant que les détails restent à affiner mais que l'orientation générale est correcte. Zvi Mowshowitz, l'un des analystes les plus suivis en matière de sécurité de l'IA et généralement sévère envers les entreprises du secteur, l'a qualifié d'« excellente proposition », arguant que le premier engagement concret — des évaluateurs externes disposant d'un accès permanent — n'est pas du tout symbolique : dans le texte d'Amodei, ces observateurs obtiennent des bureaux, des badges, des ordinateurs d'entreprise et surtout le droit de publier leurs conclusions sans contrôle éditorial de l'entreprise, des caviardages n'étant autorisés que pour des motifs de sécurité ou de secret juridique, jamais pour cacher des résultats défavorables. C'est un détail que les critiques qualifiant l'essai de simple rhétorique ont tendance à omettre : s'il est véritablement respecté, il place le pouvoir de vérification en dehors de l'entreprise, ce qu'aucun laboratoire n'avait fait jusqu me sous cette forme.
C'est le même schéma qui traverse cet article, mais à une échelle différente. OpenAI a utilisé le résultat sur Navier-Stokes également pour informer le monde du rythme de ses progrès — une formule qui construit simultanément deux choses : l'image d'une entreprise dangereusement puissante et le préalable pour demander, ensuite, à être régulée selon ses propres termes. La question posée par les critiques de l'essai d'Amodei est la même que celle que la communauté mathématique formule sur l'annonce d'OpenAI : celui qui fixe le rythme est-il vraiment en train de ralentir, ou choisit-il simplement de meilleurs mots pour décrire sa course ?
Ce qui devient rare
Le fil qui relie toute cette histoire, y compris le paradoxe du ralentissement, n'est pas « qui a raison », c'est une question plus simple : qui vérifie quoi ? Lean vérifie la déduction, pas l'énoncé. Les entreprises vérifient un modèle, pas l'intérêt général. Le Clay Institute — qui à ce jour n'a rien validé et maintient le problème marqué comme « actif » et non comme « résolu » — vérifie avec une délibération volontairement lente. Personne, pour l'instant, ne vérifie le choix du problème qui vaut réellement la peine d'être abordé, et personne, à en juger par les critiques de l'essai d'Amodei, ne vérifie si ceux qui demandent de ralentir sont vraiment en train de ralentir ou choisissent seulement avec plus de soin les mots dont ils habillent leur course.
Bryna Kra conclut sa réflexion par la question qui importe peut-être le plus : que valorisons-nous en mathématiques maintenant qu'un certain type de découverte n'est plus une ressource rare ? C'est une question qu'on peut poser en dehors des mathématiques à quiconque promet de ralentir tout en continuant, dans la même phrase, d'expliquer à quel point sa technologie est déjà irrépressible. Daniel Litt, mathématicien à l'Université de Toronto, apporte peut-être la réponse la plus constructive du dossier, en proposant de mesurer la valeur académique sur les séminaires et les débats publics plutôt que sur la seule production d'articles — car quiconque s'est contenté d'appuyer sur un bouton sans comprendre aura bien du mal à surmonter une discussion rigoureuse devant ses pairs. C'est un principe valable aussi en dehors du monde académique : la transparence se mesure à ce qui est montré étape par étape, non à ce qui est promis en paroles. Litt conclut par une phrase qu'il vaut la peine de retenir : il reste encore infiniment à apprendre ; nous avons toujours été au début, et nous le serons toujours. Cela vaut pour les mathématiques, et cela vaut peut-être aussi pour ceux qui utilisent les mathématiques comme pion dans une partie plus vaste.
Note : certaines sources citées dans cet article (publications sur Mastodon, documents PDF, publications sur X) ont été vérifiées en croisant plusieurs sources indépendantes ; lorsque le contenu original n'est plus accessible publiquement, la référence reste néanmoins traçable à travers les médias qui s'en sont fait l'écho (parmi lesquels Nature, Quanta Magazine et Axios).