francis.naukas.com
La solución de OpenAI del enunciado con forzamiento del Problema del Milenio de la ecuación de Navier–Stokes está escrita en Lean (un lenguaje de programación que permite la verificación automática de demostraciones matemáticas). Para comprobar si dicha demostración es correcta hay que analizar sus más de 423 500 líneas de código Lean repartidas en 817 archivos, que contienen 94 719 declaraciones Lean. Cualquier mínimo error conceptual (pues sabemos que no hay errores de código) en solo una de esas líneas destruiría toda la demostración. Sabemos que las IA generativas alucinan cometiendo errores conceptuales en las demostraciones largas en Lean. Pero no sabemos si en esta demostración en concreto hay alguna alucinación oculta. También sabemos que las IA generativas alucinan cuando auditan la corrección de una demostración larga en Lean de otra IA. Por ello, no podemos confiar en que una IA actual realice dicho análisis (quizás lo podrá hacer alguna futura IA mucho más poderosa dentro de un año). Por tanto, no sabemos si dicha demostración es correcta. Solo un equipo de matemáticos humanos bien financiado puede ejecutar la ingrata tarea de validación de la demostración en Lean.
Debo enfatizar que hay que validar la demostración escrita en código Lean. No se puede validar el documento escrito por IA que explica la demostración para humanos. Yo me leí dos veces las 166 páginas de dicho documento, «Finite time blowup for Navier–Stokes,» OpenAI, 08 Sep 2026 [PDF]. Los argumentos y las ideas me parecieron convincentes, pero en varios lugares la explicación me pareció incompleta. Con toda seguridad el documento se ha escrito tras leer la demostración en Lean, pero sin haber explorado la memoria de trabajo y los mensajes intercambiados entre los diez mil agentes IA que colaboraron durante 88 horas para obtener la demostración. Por ello, hay elementos clave de la demostración en Lean que están ausentes en dicho documento. Para validar la demostración por humanos hay que validar el código Lean. Porque todo el mundo sabe que las alucinaciones en la escritura de documentos científicos son uno de los grandes problemas de las IA actuales. De hecho, los artículos escritos por las IA más poderosas carecen de la elegancia y concisión de los artículos escritos por humanos. Todos los científicos lo sabemos por experiencia propia, dado que gran parte de la literatura científica actual está escrita con IA generativa.
Por ello no es sorprendente la publicación de Alexander Bastounis, Fabian Circelli, Anders C. Hansen, «Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs,» arXiv:2610.08144 [math.AP] (06 Oct 2026), doi: https://doi.org/10.48550/arXiv.2610.08144. En dicho artículo se encuentran diferencias entre el código Lean y el documento explicativo de OpenAI. Un ejemplo es una acotación del número m de derivadas del forzamiento normalizado, que en el código Lean requiere m+5 derivadas del forzamiento, mientras en el PDF de OpenAI se escribe que bastan m+4 derivadas ( en el documento en PDF )nótese que un humano nunca hubiera usado como constante), mientras que en el código Lean). Puede que te parezca una diferencia irrelevante, pero en matemáticas puede ser capital. La razón última de esta diferencia es que el documento en PDF usa una suma de Fourier convergente con decaimiento , mientras que el código Lean trabaja con una con decaimiento .
Otro ejemplo es más sustancial, para controlar un término de flujo de presión, el documento en PDF presenta una estimación que depende de una cantidad localizada , en concreto,
,
mientras que el código Lean demuestra una estimación distinta, que usa otra magnitud , relacionada con el gradiente localizado de , en concreto,
.
No hay que ser matemático para ver que la estructura de la desigualdad es completamente diferente. Lo que está validado en Lean es la segunda expresión. ¿Por qué la IA que escribió el PDF decidió modificar esta acotación? ¿Simplificó la demostración porque se puede hacer sin afectar a su corrección? ¿Cómo es posible que las diez mil IA que trabajaron no descubriesen esta simplificación?
Como titula el preprint, todo puede ser solo un «error de traducción». La demostración en Lean puede ser correcta. Pero lo que sabemos con seguridad es que el documento en PDF de OpenAI no permite inferir la demostración correcta. Para los expertos en IA esto no es algo nuevo; todos sabemos que este de alucinaciones son habituales y, lo que es peor, son inevitables. Por ello, para verificar la demostración hay que recurrir a un equipo de matemáticos que explore con todo detalle el código Lean de la demostración. Sin ayuda de IA, costará muchos años. Con ayuda de IA se puede acelerar. Pero hay que hacerlo. Y alguien tiene que financiar al equipo de investigadores que, cual quijotes, emprendan esta lucha contra los molinos que parecen gigantes.
