Navier–Stokes y la prueba en Lean: singularidades forzadas y opacidad de laboratorio

El 8 de septiembre de 2026 OpenAI declaró que uno de sus modelos internos, nunca distribuido al público, produjo una demostración de blowup en tiempo finito para las ecuaciones de Navier–Stokes tridimensionales incompresibles. La empresa difundió el documento teórico y el repositorio público NavierStokesAndEuler, que contiene la formalización en el lenguaje Lean 4 de los teoremas relativos a datos iniciales regulares sometidos a un término de forzamiento externo. Según la reconstrucción del laboratorio, el resultado cubre los enunciados de ruptura de regularidad de la formulación redactada por el matemático Charles Fefferman para el Clay Mathematics Institute, sin abordar en cambio el caso sin fuerza externa, considerado por la comunidad científica la variante más difícil del problema. El autor de la formulación oficial calificó de entusiasmante la resolución, citando las aportaciones de Córdoba y Martínez-Zoroa, mientras que la empresa aclaró desde el principio que no pretende reclamar el premio de un millón de dólares.

La operación entrelaza la automatización matemática con los tiempos de las instituciones académicas. El Clay Mathematics Institute sigue incluyendo Navier–Stokes entre los problemas sin resolver: el reglamento exige la publicación en una sede cualificada, una espera de al menos dos años desde la publicación y la aceptación general por parte de la comunidad matemática, sin que el instituto se haya pronunciado hasta ahora sobre el fondo. Su presidente, Martin Bridson, ha recordado que la evaluación sigue a propósito un ritmo sin prisas, para garantizar un rigor absoluto. Complica el cuadro una controversia de prioridad con un trabajo paralelo expuesto por el matemático Terence Tao y descrito por sus autores como fuertemente asistido por inteligencia artificial. Un matemático de la Universidad de Nueva York ha cuestionado la reconstrucción de los contactos ofrecida por el laboratorio, planteando que sesiones privadas con una herramienta propietaria hayan podido contribuir al resultado; la empresa ha desmentido haber visto directamente el trabajo no publicado, aunque admite que no puede descartar el impacto de datos de uso desidentificados en el entrenamiento de sus modelos.

El repositorio incluye las instrucciones para que la demostración se vuelva a comprobar a máquina, pero hasta ahora no consta ninguna verificación independiente concluida; más allá de ese control, la naturaleza propietaria de la infraestructura empleada impide cualquier verificación independiente sobre los costes y las métricas de eficiencia exhibidas. El cálculo declarado —unos diez mil agentes concurrentes entre el 1 y el 5 de septiembre, con 88 horas para llegar a la demostración y otras 17 para la formalización y la verificación en Lean— sigue confinado a afirmaciones corporativas que nadie puede reproducir desde fuera. Sin acceso al código de entrenamiento ni a los pesos del sistema, la comunidad científica solo puede validar los pasos formales depositados en el repositorio, dejando en la sombra las condiciones reales de reproducibilidad del experimento.

La matemática formal encuentra un aliado formidable en el control automático de los pasos lógicos, pero la carrera por la primogenitura científica mediante modelos cerrados muestra sus límites estructurales. Verificar un teorema es ya una tarea que ejecuta una máquina; establecer la transparencia de la cadena que lo generó exige todavía un rigor enteramente humano.

— Olya