Navier-Stokes : la preuve d'OpenAI mise en doute
Original : Navier–Stokes Lost in Translation
Pourquoi c'est important
Remet en question la validité des annonces de preuves mathématiques générées par IA via Lean.
Des chercheurs publient sur arXiv que la vérification Lean de l'autoformalisation IA ne garantit pas la validité d'une preuve en langage naturel, citant la preuve Navier-Stokes d'OpenAI comme exemple de traduction défaillante.
Alexander Bastounis, Fabian Circelli et Anders C. Hansen (arXiv:2610.08144, 6 octobre 2026) s'attaquent directement à une pratique en plein essor : l'autoformalisation, où un système IA traduit un texte mathématique en langage naturel vers un langage formel comme Lean, puis soumet le résultat à une vérification mécanique. OpenAI avait annoncé une preuve de l'explosion des solutions aux équations de Navier-Stokes via ce processus.
Les auteurs démontrent que la résolution des ambiguïtés propres au langage mathématique naturel — étape indispensable pour une traduction sémantiquement fidèle — est indécidable, classée au sommet de la hiérarchie SCI (Solvability Complexity Index), notée SCI = ∞. En clair : ce problème est strictement plus difficile que le problème de l'arrêt (Halting problem, SCI = 1), lui-même non calculable.
Pour appuyer leur thèse, les chercheurs fournissent plusieurs exemples concrets de mauvaises traductions IA vers Lean, où la preuve formalisée vérifiée ne correspond pas à la preuve en langage naturel d'origine. Concernant Navier-Stokes spécifiquement, ils affirment que la preuve Lean formalisée ne correspond pas à la preuve NL d'explosion des solutions annoncée par OpenAI. L'article de 25 pages, accompagné de 4 figures, remet ainsi en cause la fiabilité de toute chaîne de validation reposant sur l'autoformalisation IA comme garantie de correction mathématique.