Des chercheurs relèvent des écarts dans la preuve Lean d'OpenAI sur Navier-Stokes

Des chercheurs ont confronté la preuve publiée par OpenAI sur les équations de Navier-Stokes à sa version formalisée en Lean, et ont relevé des écarts à plusieurs endroits clés. La version vérifiable par machine y démontre des énoncés plus faibles que ceux affichés dans le texte destiné aux humains. Les équations de Navier-Stokes figurent parmi les sept « problèmes du millénaire » du Clay Mathematics Institute, dont chacun est doté d'un prix de 1 million de dollars : la moindre fissure dans un tel résultat se remarque donc immédiatement. Ce n'est pas, à ce stade, une réfutation.

Ce que les chercheurs ont découvert

Le principe de la vérification est simple. On prend l'article contenant la preuve et, en parallèle, une version formelle écrite en Lean, c'est-à-dire dans un langage où chaque étape du raisonnement est vérifiée par ordinateur. Si les deux versions décrivent la même chose, elles coïncident. Ici, elles divergent : en plusieurs points nodaux, la version Lean affirme moins que le texte.

La description de la vérification ne précise pas si le travail d'OpenAI prétend résoudre entièrement le problème du Clay Institute ou n'établir qu'un résultat plus restreint. L'ampleur de l'annonce doit se juger sur la publication elle-même, et cette réserve est importante. Elle ne change toutefois pas la conclusion : l'artefact formel doit correspondre à ce qui est promis dans l'article.

Pourquoi un « énoncé plus faible » est un problème sérieux

Lean n'accepte pas d'arguments du type « c'est évident » ou « cela découle de considérations standard ». Si une preuve passe la vérification, elle est correcte par rapport à ce qui est précisément écrit dans la formalisation. La question centrale est donc de savoir si la version formelle démontre la même chose que ce qui est affirmé en toutes lettres. Lorsque la formulation dans le code est plus faible que dans l'article, plusieurs scénarios sont possibles :

• les formalisateurs ont simplifié les hypothèses pour mener le travail à son terme, sans le dire ;
• le théorème est formulé de façon imprécise dans le texte, et la version Lean montre ce qui a réellement été prouvé ;
• une étape qui paraît démontrée dans l'article ne tient pas à l'épreuve d'une vérification rigoureuse ;
• l'écart s'explique par une discordance technique entre définitions, que l'on corrige par un ajustement.

Le premier et le quatrième cas sont sans gravité, le troisième est dangereux. Tant que les auteurs ou des experts indépendants n'ont pas examiné chaque point séparément, il est impossible de trancher entre ces scénarios.

Les faits clés à partir des données disponibles :

• objet de la vérification : la preuve d'OpenAI sur les équations de Navier-Stokes ;
• méthode : comparaison du texte publié avec la version Lean algorithmique ;
• résultat : des écarts à plusieurs endroits clés ;
• nature des écarts : les énoncés sont plus faibles dans la version machine ;
• statut : ce n'est pas encore une réfutation, mais un motif de doute.

Ce qu'il faut surveiller ensuite

Si vous suivez l'IA appliquée aux mathématiques, quelques repères sont utiles. Premier point : la réaction d'OpenAI. Une analyse claire de chaque écart, qu'il s'agisse d'une formulation corrigée, d'un code Lean mis à jour ou de la reconnaissance de limites, en dira plus que n'importe quelle déclaration générale. Deuxième point : ce que diront les spécialistes de la mécanique des fluides et des équations aux dérivées partielles. La vérification formelle contrôle la logique, mais seuls des mathématiciens du domaine peuvent juger si le sens du problème s'est perdu en chemin. Troisième point : la formalisation et les documents associés seront-ils publiés, afin que la vérification puisse être reproduite de manière indépendante ?

Pour ceux qui prennent des décisions sur la base de telles annonces, la conclusion est pratique. Un résultat obtenu par IA en mathématiques ne doit être tenu pour confirmé que lorsqu'une vérification indépendante existe et que la version formelle correspond au théorème annoncé. Un communiqué de presse et un preprint n'y suffisent pas. Tant que les écarts ne sont pas levés, l'affaire Navier-Stokes reste une annonce retentissante, et non un fait acquis.