Navier–Stokes et la preuve en Lean : singularités forcées et opacité de laboratoire

Le 8 septembre 2026, OpenAI a déclaré qu'un de ses modèles internes, jamais mis à disposition du public, avait produit une démonstration d'explosion en temps fini pour les équations de Navier–Stokes tridimensionnelles incompressibles. L'entreprise a diffusé le document théorique et le dépôt public NavierStokesAndEuler, qui contient la formalisation en langage Lean 4 des théorèmes portant sur des données initiales régulières soumises à un terme de forçage externe. Selon la reconstitution du laboratoire, le résultat couvre les énoncés de perte de régularité de la formulation rédigée par le mathématicien Charles Fefferman pour le Clay Mathematics Institute, sans aborder toutefois le cas sans force externe, tenu par la communauté scientifique pour la variante la plus difficile du problème. L'auteur de la formulation officielle a qualifié la résolution d'enthousiasmante, en citant les contributions de Córdoba et Martínez-Zoroa, tandis que l'entreprise a précisé d'emblée qu'elle ne réclamerait pas le prix d'un million de dollars.

L'opération entremêle l'automatisation mathématique et le tempo des institutions académiques. Le Clay Mathematics Institute continue de classer Navier–Stokes parmi les problèmes non résolus : le règlement exige une publication dans un lieu qualifié, une attente d'au moins deux ans après la publication et une acceptation générale par la communauté mathématique, l'institut ne s'étant jusqu'ici pas prononcé sur le fond. Son président, Martin Bridson, a rappelé que l'évaluation suit délibérément un rythme sans hâte, afin d'en garantir la rigueur absolue. Le tableau se complique d'une controverse de priorité avec un travail parallèle exposé par le mathématicien Terence Tao et décrit par ses auteurs comme fortement assisté par l'intelligence artificielle. Un mathématicien de l'université de New York a contesté la reconstitution des contacts fournie par le laboratoire, en avançant que des sessions privées avec un outil propriétaire auraient pu contribuer au résultat ; l'entreprise dément avoir vu directement le travail non publié, tout en admettant ne pas pouvoir exclure l'effet de données d'usage dépersonnalisées sur l'entraînement de ses propres modèles.

Le dépôt indique la marche à suivre pour faire revérifier la démonstration par la machine, mais aucune vérification indépendante n'est à ce jour achevée ; au-delà de ce contrôle, la nature propriétaire de l'infrastructure employée interdit toute vérification indépendante des coûts et des métriques d'efficacité brandies. Le calcul déclaré — environ dix mille agents concurrents entre le 1er et le 5 septembre, 88 heures pour parvenir à la démonstration et 17 de plus pour la formalisation et la vérification en Lean — reste cantonné à des affirmations d'entreprise que personne ne peut reproduire de l'extérieur. Sans accès au code d'entraînement ni aux poids du système, la communauté scientifique ne peut valider que les étapes formelles déposées sur le dépôt, laissant dans l'ombre les conditions réelles de reproductibilité de l'expérience.

Les mathématiques formelles trouvent un allié redoutable dans le contrôle automatique des enchaînements logiques, mais la course à l'antériorité scientifique par modèles fermés montre ses limites structurelles. Vérifier un théorème est désormais une tâche exécutable par une machine ; établir la transparence de la chaîne qui l'a produit réclame encore une rigueur tout humaine.

— Olya