OpenAI dice haber resuelto Navier‑Stokes: qué demuestra Lean, qué reconoce Clay y qué todavía no está cerrado

OpenAI afirma haber resuelto uno de los problemas matemáticos más famosos del mundo: la existencia y regularidad de las ecuaciones tridimensionales de **Navier-Stokes**. La compañía ha publicado una demostración y una versión formalizada en **Lean**, un sistema que comprueba pruebas matemáticas paso a paso.

La reacción más importante no viene de OpenAI, sino del **Clay Mathematics Institute**, custodio de los Problemas del Milenio. El 11 de septiembre declaró que el problema **'aparentemente ha sido resuelto'**, pero añadió que el proceso de evaluación y asignación de crédito será deliberadamente lento.

Esa frase evita dos extremos. No estamos ante una simple ocurrencia de un chatbot, porque existe un manuscrito completo, una formalización y una reacción pública del organismo responsable del problema. Pero tampoco existe todavía una proclamación definitiva ni un premio concedido.

Lee también: OpenAI dice que su IA aceleró partes del diseño de un chip, no que lo diseñara sola · Documentos del pleito del NYT muestran inquietud interna en Microsoft y OpenAI por el uso de prensa para entrenar IA

OpenAI dice que el sistema encontró una construcción en la que una solución suave puede desarrollar una **singularidad en tiempo finito** bajo una de las formulaciones aceptadas del problema. En términos intuitivos, demostrar una singularidad significa mostrar que la evolución matemática puede dejar de permanecer regular bajo las condiciones consideradas.

¿Qué aporta Lean? Una demostración tradicional puede contener un salto lógico difícil de detectar. Lean obliga a traducir la prueba a reglas formales que el ordenador puede comprobar. Si el fichero es aceptado, ofrece una garantía muy fuerte de que los pasos formalizados son lógicamente coherentes.

Pero **formalizar no resuelve automáticamente toda la discusión matemática**. Todavía hay que comprobar que las definiciones, hipótesis y objetos formalizados corresponden exactamente con la formulación relevante del problema y que no existe una discrepancia conceptual escondida en el punto de partida.

OpenAI describe además una escala de cómputo poco habitual en investigación matemática: grupos de agentes coordinados, del orden de **10.000 agentes concurrentes** en la fase de Navier-Stokes, millones de mensajes y alrededor de 130.000 millones de tokens de salida para ese problema.

La compañía afirma que la búsqueda principal duró unas **88 horas** y que la formalización y verificación en Lean necesitó otras 17 horas. La cifra no significa que la IA 'pensara durante cuatro días como un matemático humano': describe una enorme cantidad de trabajo paralelo computacional.

También existe un debate de atribución. OpenAI reconoce trabajo concurrente de Levent Alpöge y Tristan Buckmaster sobre ecuaciones de Euler y afirma que sus datos privados no influyeron en el sistema. Parte de la comunidad matemática discute cómo debe reconocerse el conocimiento humano que alimenta o guía este tipo de descubrimientos.

La conclusión prudente es extraordinaria sin necesidad de exagerarla: **un instituto matemático de referencia considera que el problema parece resuelto, una IA produjo una prueba formalizable y ahora empieza la parte lenta de la ciencia: revisar, comprender, atribuir y decidir qué significa realmente el resultado.**