Contexte et objectif

Le manuscrit Navier–Stokes lost in translation, soumis le 6 octobre 2026 et long de 25 pages avec quatre figures, examine l’usage croissant de l’auto‑formalisation pour vérifier des textes mathématiques générés par IA. Les auteurs – Alexander Bastounis, Fabian Circelli et Anders C. Hansen – s’appuient sur l’exemple annoncé par OpenAI d’une preuve de blow‑up des solutions de Navier‑Stokes traduite en Lean. L’objectif déclaré est de montrer que la simple validation mécanique d’un code Lean ne suffit pas à garantir la fidélité du raisonnement original exprimé en langage naturel (NL).

Limites de l’autoformalisation

Le processus étudié comporte deux étapes critiques : la traduction du texte NL vers le langage formel Lean, puis la vérification automatisée du script Lean. Les auteurs soulignent que la traduction doit résoudre des ambiguïtés sémantiques inhérentes aux énoncés mathématiques. Or, aucune IA actuelle ne peut assurer une résolution exhaustive de ces ambiguïtés, ce qui conduit à des « mistranslations » concrètes. Le papier fournit plusieurs exemples où le texte Lean vérifié diverge du raisonnement NL, notamment dans la preuve de Navier‑Stokes où le script Lean ne correspond pas aux arguments de blow‑up présentés par OpenAI.

Analyse de la complexité SCI

Un point central de l’article est la localisation du problème de désambiguïsation dans la hiérarchie du Solvability Complexity Index (SCI). Les auteurs affirment que ce problème se situe à un niveau « arbitrarily high », c’est‑à‑dire que son SCI est égal à l’infini. En comparaison, le problème de l’arrêt possède un SCI = 1. Cette différence indique que fournir une traduction sémantiquement fidèle est, du point de vue de la théorie de la calculabilité, plus difficile que tout problème décidable, y compris le problème de l’arrêt. Cette conclusion repose sur les classifications MSC : 35Q30 (équations de Navier‑Stokes) et 03Dxx (théorie de la calculabilité), ainsi que sur les classes secondaires 68V20 (IA) et 03B65 (arithmétique).

Illustrations avec la preuve Navier‑Stokes

Pour étayer leur thèse, les auteurs détaillent comment le script Lean fourni par OpenAI vérifie formellement une série de lemmes qui, dans le texte NL, sont censés conduire à la singularité des solutions. Cependant, l’analyse montre que certains lemmes formalisés ne sont pas dérivés des hypothèses NL, ou que des hypothèses implicites du texte NL sont omises dans la version Lean. Cette discordance signifie que la preuve mécanique, bien que correcte dans l’univers Lean, ne valide pas la preuve naturelle. Le papier conclut que, sans une garantie de traduction fidèle, la vérification Lean ne peut être considérée comme une preuve fiable du résultat NL.