La afirmación de OpenAI sobre Navier–Stokes viene con prueba en Lean. Su origen está en disputa.

OpenAI publicó el martes un artículo titulado “On the Navier–Stokes Millennium Prize Problem”, en el que dice compartir una solución generada por IA a uno de los siete problemas del milenio, junto con un texto explicativo y una demostración formal en Lean. Ese mismo día, más temprano, el profesor de matemática de NYU Tristan Buckmaster anunció tres demostraciones propias, junto al matemático de Anthropic Levent Alpöge — y afirmó que OpenAI se enteró del enfoque que ellos venían trabajando sin publicar, lo llevó primero hasta la ecuación más difícil y después lo presionó por la autoría.

Qué se demostró exactamente

Las ecuaciones de Navier–Stokes describen cómo se mueven los fluidos, y el problema del milenio plantea algo que suena simple: si se parte de condiciones suaves, ¿las soluciones se mantienen suaves para siempre o pueden romperse en tiempo finito? La respuesta de OpenAI es que pueden romperse.

La formalización en Lean publicada junto al texto, en el repositorio openai/NavierStokesAndEuler, enuncia el resultado con precisión. Para cualquier viscosidad positiva, demuestra que existen datos iniciales suaves y un término de forzado suave en ℝ³ para los cuales ninguna solución suave global mantiene su energía cinética uniformemente acotada, y por separado que lo mismo vale para datos periódicos suaves en el toro ℝ³/ℤ³. El repositorio indica que esto corresponde a las alternativas (C) y (D) de la descripción oficial del problema del Clay Mathematics Institute.

El término de forzado es el detalle a retener. Las alternativas (C) y (D) son las ramas de “ruptura” del enunciado oficial y permiten aplicar una fuerza externa al fluido. Buckmaster, que había elegido el mismo camino, lo describió así en el texto con el que anunció sus propias demostraciones:

The route to the Clay problem through a smooth force, options c and d in Fefferman's statement of the problem, is the route Luis and Diego opened and the one Levent and I had quietly chosen to attack.

El mismo repositorio incluye además un resultado sobre Euler sin ningún forzado: una velocidad inicial suave, de soporte compacto y con divergencia nula en ℝ³ que desarrolla una singularidad en tiempo finito, con la norma C¹ volviéndose no acotada y la integral de vorticidad divergiendo. Esa distinción — forzado contra no forzado — importa tanto para la disputa como para la matemática.

Una demostración verificable por máquina no es una demostración zanjada

La formalización apunta a Lean 4.34.0-rc2 con Mathlib, y el repositorio incluye un directorio ComparatorChallenges con instrucciones para verificar la prueba de manera independiente. Es más de lo que ofrece la mayoría de los supuestos avances el primer día: cualquiera con el toolchain puede correr la verificación en vez de creer en la palabra de la empresa.

Conviene ser preciso sobre qué garantiza esa verificación. Lean confirma que la demostración se sigue del enunciado tal como fue formalizado. No confirma que ese enunciado formal sea el que la comunidad matemática entiende por el problema del milenio, ni verifica el texto en prosa que lo acompaña. Contrastar los enunciados formales con la redacción oficial de Charles Fefferman — incluido si el término de forzado cumple las cotas que el enunciado exige — es trabajo humano, y todavía no ocurrió. El artículo se publicó hoy; no hubo revisión por pares.

La disputa por el crédito

Según TechCrunch, que publicó el relato de Buckmaster el martes, él y Alpöge estaban terminando sus propios resultados cuando supieron que “information about our progress had been passed to OpenAI” (“información sobre nuestro avance había llegado a OpenAI”). Cuando hicieron contacto, les dijeron que OpenAI ya tenía una demostración completa del problema central. Las repreguntas sobre cuándo había empezado OpenAI y cuánta intervención humana hubo, cuenta Buckmaster, recibieron respuestas evasivas.

Su sospecha se apoya en lo inusual del enfoque. “Casi nadie que yo conozca estaba trabajando en eso”, dijo sobre el camino del forzado suave. “No es la dirección a la que se llega en pocos días dándole a un modelo el enunciado del problema”.

Buckmaster afirma además que Sébastien Bubeck, que dirige el equipo de matemática de OpenAI, propuso sacar a Alpöge — empleado de Anthropic, aunque no trabajando en nombre de la empresa — de los créditos como parte de un acuerdo, y que cuando dijo que haría pública la disputa, Bubeck le respondió “¿Por qué arruinarías tu carrera?” y luego “Si no querés que sea amable, no tengo por qué serlo”. Son las caracterizaciones que hace Buckmaster de conversaciones privadas. No pudimos abrir una fuente con la respuesta del propio Bubeck, y corresponde leerlas como el relato de una sola de las partes.

El artículo de OpenAI aborda la cuestión del origen de manera directa, en un pasaje que cita TechCrunch:

We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models. However, our proofs differ significantly and even the precise results proved are different in the Euler case (forced vs unforced).

El texto también confirma que el esfuerzo de OpenAI arrancó el 1 de septiembre, motivado por rumores de que dos problemas del milenio habían sido resueltos, y que hubo conversaciones con Buckmaster y Alpöge. TechCrunch informa que la semana de trabajo consumió 300.000 millones de tokens de salida entre varios problemas, lo que estima en unos 22,5 millones de dólares si se cobrara a las tarifas actuales de la API de Astra. El Clay Mathematics Institute asigna un premio de un millón de dólares a cada uno de los siete problemas.

Qué cambia para quienes construyen con estas herramientas

Dos de las lecciones acá son prácticas antes que matemáticas.

• La verificación formal se está volviendo la forma creíble de publicar un resultado producido por IA. Un archivo Lean que cualquiera puede correr dice más que un número de benchmark, y es el artefacto a pedir cuando la salida de un modelo tiene que ser confiable y no solo revisada por encima.
• Las transcripciones de los agentes de código son un tema de gobierno de datos, no solo de privacidad. TechCrunch señala que OpenAI se reserva el derecho de entrenar con las interacciones de Codex, con una opción para desactivarlo, y que Buckmaster usó Codex intensivamente sobre trabajo sin publicar. Haya pasado lo que haya pasado en este caso, la lección general vale: si trabajás en algo novedoso o confidencial dentro del agente de código de un laboratorio, revisá la configuración de retención y entrenamiento antes de empezar, no después.
• La escala pasó a ser una estrategia, no solo una línea de costo. Una semana de agentes en paralelo con 300.000 millones de tokens de salida es un método al alcance de muy pocas organizaciones, y cambia quién puede llegar primero una vez que el enfoque se conoce.

Nada de esto zanja la matemática. La demostración es pública y verificable por máquina, así que las próximas semanas de lectura especializada van a definir si los enunciados formales se corresponden con el problema que planteó Clay, y si una construcción con forzado se acepta como resolución o como un resultado fuerte pero contiguo. La cuestión del crédito, si se resuelve, la van a resolver personas y no Lean.

Una nota sobre las fuentes: la página del artículo de OpenAI bloquea a los clientes automatizados, así que no la leimos directamente. Verificamos el anuncio, su título y su marca temporal en el propio feed de novedades de OpenAI, leimos el repositorio Lean publicado y nos apoyamos en las citas textuales que TechCrunch toma del artículo.