Una IA de OpenAI propone resolver el problema de Navier-Stokes

OpenAI informó este 8 de septiembre que uno de sus modelos produjo una propuesta de solución para el problema de existencia y suavidad de Navier-Stokes, uno de los siete Problemas del Milenio. La empresa publicó un desarrollo en lenguaje matemático y una formalización en Lean, un asistente que comprueba inferencias paso a paso.

Las ecuaciones de Navier-Stokes describen el movimiento de fluidos como aire y agua. El desafío no consiste en calcular un caso cotidiano, sino en demostrar para datos iniciales adecuados si siempre existen soluciones suaves en tres dimensiones o si puede aparecer una singularidad. El Clay Mathematics Institute ofrece un premio de un millón de dólares.

Una prueba formal reduce una clase de errores porque Lean exige que cada paso derive de reglas y definiciones explícitas. Sin embargo, el software verifica la formulación que recibe. Matemáticos independientes deben confirmar que las definiciones representan exactamente el problema original, que no se agregaron supuestos y que las bibliotecas usadas son correctas.

La guía para interpretar el anuncio distingue propuesta, verificación y reconocimiento. OpenAI puede publicar una prueba propuesta; Lean puede aceptar su estructura formal; la comunidad debe revisar el significado y el Clay Institute aplica sus propias reglas. Ninguna de esas etapas convierte automáticamente el trabajo en una solución oficialmente reconocida.

La formalización resulta especialmente relevante para modelos de lenguaje, que pueden redactar argumentos plausibles con huecos difíciles de detectar. Un asistente de pruebas obliga a exponer pasos que de otro modo quedarían implícitos. Aun así, una cadena mecánicamente válida puede partir de una definición equivocada o resolver una variante más débil.

El anuncio llega después de trabajos donde modelos de IA colaboraron en problemas matemáticos abiertos y usaron herramientas como Lean. La novedad aquí es la escala simbólica y científica del objetivo. Navier-Stokes tiene vínculos profundos con análisis, turbulencia y física matemática, y ha resistido décadas de trabajo especializado.

La revisión no será inmediata. Especialistas deberán reconstruir el argumento, comparar cada hipótesis con el enunciado oficial y buscar pasos circulares o resultados auxiliares no demostrados. También importa que los archivos formales sean reproducibles con versiones públicas del verificador y de sus dependencias.

Hasta completar ese proceso, la formulación correcta es que una IA propuso una solución, no que resolvió definitivamente el problema. Si supera la revisión, sería un hito tanto matemático como metodológico. Si falla, el material todavía puede revelar ideas útiles y mostrar dónde los sistemas formales ayudan a auditar investigación generada por IA.

El proceso formal además debe distinguir entre axiomas estándar y resultados introducidos específicamente para la demostración. Un archivo puede compilar porque acepta una afirmación fuerte como supuesto. La auditoría necesita identificar cada dependencia, comprobar que no contiene el resultado buscado de forma equivalente y verificar que la conclusión corresponde al caso tridimensional exigido por el desafío original.