El 8 de septiembre de 2026, OpenAI publicó una prueba analítica y una formalización en Lean que, según la empresa, resuelven el problema de existencia y suavidad de Navier–Stokes mediante las alternativas C y D de la formulación oficial del Clay Mathematics Institute. El resultado construye una solución tridimensional incompresible que parte del reposo, recibe una fuerza externa suave y desarrolla velocidad no acotada en tiempo finito, mientras la energía cinética permanece uniformemente acotada. Es mucho más que una conjetura generada por IA, pero todavía no equivale a un reconocimiento definitivo por parte de la comunidad matemática ni del Clay.
La clave es separar tres cosas que a menudo aparecen mezcladas en los titulares: la afirmación matemática publicada, la verificación formal de una versión del teorema en Lean y la validación independiente necesaria para que expertos e instituciones acepten que la formalización corresponde exactamente al problema y que toda la construcción resiste el escrutinio.
Qué afirma demostrar la prueba de OpenAI
El artículo “Finite Time Blowup for Navier–Stokes” presenta, para toda viscosidad positiva, una fuerza suave de soporte compacto y campos de velocidad y presión que permanecen suaves hasta un tiempo singular. La construcción comienza con velocidad inicial cero. A medida que el tiempo se acerca al instante singular, la norma máxima de la velocidad crece sin límite mientras la norma de energía se mantiene acotada.
En términos menos técnicos, la construcción describe un vórtice que se contrae y gira cada vez más rápido. El reto no consiste simplemente en elegir una fuerza externa que también se vuelva infinita: el artículo busca que la propia dinámica no lineal del fluido produzca el crecimiento mientras la fuerza residual sigue siendo suave. OpenAI afirma que este mecanismo establece la alternativa C en el espacio completo y, gracias al soporte compacto, también la alternativa D en el caso periódico.
Por qué la fuerza externa no vuelve irrelevante el resultado
Una fuente importante de confusión es tratar “forzado” como si significara automáticamente un problema distinto al del Premio del Milenio. La formulación oficial del Clay permite, en las alternativas C y D de ruptura, una fuerza externa suave que cumpla condiciones de regularidad y decaimiento. Por lo tanto, si la construcción publicada satisface realmente todas esas hipótesis, usar una fuerza suave no descalifica la estrategia.
Esto también significa que no debe atribuirse al resultado algo más fuerte de lo que se demostró. No prueba que todo flujo suave sin fuerza externa desarrolle singularidades, ni que un vaso de agua real vaya a alcanzar velocidad infinita. La afirmación es existencial: existe una configuración matemática admisible en la que una solución suave no puede prolongarse globalmente bajo los requisitos de la formulación.
Qué papel cumple Lean
OpenAI publicó un repositorio con certificados en Lean 4 para los resultados de Navier–Stokes y Euler. En un sistema como Lean, un guion de prueba se transforma en un objeto lógico que es comprobado por un núcleo pequeño. Cuando la compilación y la comprobación tienen éxito, el núcleo acepta que el teorema formal se deriva de las definiciones, teoremas importados y axiomas declarados en el entorno.
Esto ofrece una protección muy fuerte frente a muchos tipos de errores en pruebas largas: objetivos sin cerrar, pasos que no se deducen de las hipótesis o fallos ocultos en tácticas no pueden pasar simplemente como una demostración válida una vez que el término final es revisado por el núcleo. La propia documentación de Lean, sin embargo, subraya un límite crucial: la comprobación solo tiene el significado deseado si la declaración formal corresponde correctamente a la afirmación matemática informal y si las definiciones y dependencias usadas significan lo que se supone que significan.
El repositorio de OpenAI también incluye instrucciones para una comprobación independiente con Comparator, una herramienta que puede reconstruir y volver a revisar el certificado en un entorno más controlado y con verificadores externos. Publicar ese material facilita auditorías reproducibles, pero ofrecer una ruta de comprobación no es lo mismo que afirmar que toda la comunidad matemática ya ha completado esa auditoría.
Las tres capas de validación que no deben confundirse
| Capa | Qué establece | Qué todavía debe examinarse |
|---|---|---|
| Prueba analítica publicada | Existe una construcción matemática detallada con un teorema explícito y una cadena de argumentos. | Los especialistas deben revisar estimaciones, hipótesis, correcciones, límites y posibles lagunas. |
| Formalización en Lean | El núcleo puede verificar que el certificado deriva la declaración formal a partir del entorno lógico utilizado. | Hay que auditar que la declaración formal, las definiciones y las dependencias representan exactamente las condiciones del Clay. |
| Reconocimiento matemático e institucional | Surge cuando el resultado supera el examen independiente y obtiene una aceptación amplia. | Las reglas del Clay exigen publicación en un medio calificado, al menos dos años y aceptación general antes de una posible revisión para el premio. |
Qué permite decir ahora la reacción independiente
La cobertura de Nature del 8 de septiembre trató el anuncio como una afirmación de enorme importancia, no como una certificación editorial de que el problema ya está definitivamente cerrado. El artículo recogió reacciones iniciales positivas de matemáticos, entre ellos el presidente del Clay Mathematics Institute, Martin Bridson, y el especialista Luis Martínez Zoroa. Esas reacciones muestran que el trabajo está siendo tomado en serio, pero no sustituyen una revisión detallada.
Esta distinción importa porque una prueba de 166 páginas acompañada por una formalización extensa puede ser plausible, impresionante y, al mismo tiempo, encontrarse todavía al comienzo del escrutinio. En matemáticas, pasar de “se publicó una prueba” a “el problema se acepta como resuelto” depende de que especialistas puedan reconstruir, poner a prueba y comparar los argumentos de manera independiente.
Por qué el Clay Mathematics Institute no decide esto de inmediato
Las reglas del Premio del Milenio son deliberadamente lentas. El Clay no acepta una solución propuesta para una evaluación directa e inmediata. Antes de considerar una, exige que la solución se publique en un medio calificado, que hayan transcurrido al menos dos años desde esa publicación y que haya alcanzado aceptación general en la comunidad matemática mundial. Solo después puede el instituto realizar su propio examen.
OpenAI ha declarado que no pretende reclamar el premio de US$1 millón. Aun así, las reglas ayudan a entender el estado de la noticia: la corrección matemática puede discutirse mucho antes del reconocimiento institucional, y el reconocimiento institucional, por diseño, no ocurre el día del anuncio.
Entonces, ¿Navier–Stokes fue resuelto por IA?
La respuesta más precisa al 9 de septiembre de 2026 es: OpenAI ha presentado una candidata a solución muy sustancial, con una prueba analítica pública y un certificado formal en Lean, que afirma resolver las alternativas C y D del problema oficial. Si la correspondencia entre el teorema formalizado y la formulación del Clay es correcta y los argumentos resisten el escrutinio independiente, esto constituiría una resolución del Problema del Milenio mediante una construcción encontrada por un sistema de IA.
Lo que todavía no puede afirmarse sin matices es que el resultado ya haya recibido una validación matemática amplia o el reconocimiento del Clay. Lean reduce de forma drástica el riesgo de ciertos errores lógicos dentro de la formalización, pero no sustituye la tarea humana de comprobar que lo formalizado es exactamente el teorema relevante, que las definiciones tienen el significado previsto y que el resultado encaja por completo en las reglas del problema original.
