OpenAI publicó el martes que un modelo interno —de los que no puedes llamar por API— había producido una explosión en tiempo finito para las ecuaciones de Navier–Stokes en tres dimensiones. Unos 10.000 agentes en paralelo, 88 horas de reloj entre el 1 y el 5 de septiembre, 2,7 millones de mensajes y algo así como 130.000 millones de tokens de salida.

Después, todo aquello se formalizó en Lean y una máquina lo verificó en otras diecisiete horas.

Y para cuando la mayoría había terminado de leer el anuncio, la historia ya no iba de fluidos.

Qué dice realmente el teorema

Navier–Stokes describe cómo se mueve un fluido. La pregunta del milenio es si un fluido que empieza siendo suave sigue siéndolo para siempre, o si las ecuaciones pueden comerse a sí mismas: alguna magnitud disparándose a infinito en un punto y en tiempo finito. Eso es una explosión, y es la diferencia entre "este modelo siempre tiene sentido físico" y "este modelo tiene un agujero que no hemos encontrado nunca".

El enunciado oficial de Charles Fefferman son cuatro afirmaciones, no una. (A) y (B) dicen que las soluciones se mantienen suaves para siempre, en todo el espacio y en el toro periódico respectivamente, sin ninguna fuerza externa. (C) y (D) son las versiones de ruptura, y ahí el enunciado sí permite una fuerza externa suave y bien portada. Demuestra o refuta cualquiera de las cuatro y el problema queda resuelto.

OpenAI demostró (C) y (D). Unas cien páginas, partiendo de un fluido en reposo, con una fuerza suave aplicada, energía finita durante todo el proceso, y una singularidad igualmente.

Así que, según la letra del reglamento: sí, eso es una resolución. Quiero ser justo con esto porque internet lleva dos días siendo injusto en ambas direcciones a la vez.

Pero cuando un matemático dice el problema de Navier–Stokes en voz alta, está pensando en (A) o en (B). Sin nadie empujando. Que se te permita seguir empujando el fluido durante toda la ejecución es una ayuda, aunque el empujón tenga que ser suave y de energía finita. Es la diferencia entre demostrar que tu servicio se cae con su propia carga en régimen estacionario y demostrar que se cae si además puedes inventarte tráfico nuevo sobre la marcha. Las dos son caídas reales. Solo una te dice que la cosa está rota por sí sola.

La fuerza es el asterisco. Es un resultado legítimo y está en el reglamento oficial, y tampoco es la versión que lleva noventa años resistiéndose.

Diecisiete horas

Y aquí la parte que está recibiendo, tirando por lo alto, una décima parte de la atención que merece.

Cien páginas de demostración de algo de este tamaño significan normalmente uno o dos años de revisores. Seminarios. Alguien encontrando un hueco en la página 61 al noveno mes. Lo de Perelman con Poincaré necesitó que se escribieran volúmenes enteros de exposición solo para poder comprobarlo, y eso llevó años.

Esta venía con una formalización en Lean y un kernel que le daba la razón. Eso no es "a los revisores les ha parecido convincente". Es verdad en el mismo sentido en que tu build pasa: una máquina recorrió mecánicamente cada paso hasta los axiomas y no protestó.

El paso históricamente caro, ¿esto es correcto?, se quedó en un error de redondeo. Diecisiete horas. Todos los demás pasos del proceso siguen costando exactamente lo mismo que la semana anterior.

Y esta forma la conocemos. Es cualquier repo donde CI se volvió rápido y las PR siguen tres semanas paradas, porque la discusión nunca fue sobre si pasan los tests. Era sobre propiedad, sobre alcance y sobre quién tiene derecho a decir que sí. Haz gratis la mitad verificable por máquina y no eliminas el cuello de botella: te enteras de cuál era el cuello de botella de verdad.

Aquí resultó ser la lista de autores.

La parte que el kernel no puede comprobar

Tristan Buckmaster, de la NYU, y Levent Alpöge —matemático de Harvard, hoy en el equipo técnico de Anthropic— llevaban cosa de un año con esta familia de ecuaciones, apoyándose en Claude, Codex y Astra. El 7 de septiembre publicaron tres resultados de explosión: medios porosos incompresibles, Boussinesq y Euler incompresible en tres dimensiones, que es el primo sin viscosidad del problema de verdad. Con formalizaciones en Lean, por cierto.

La tirada de OpenAI arrancó el 1 de septiembre, después de que corriera el rumor de que esos dos tenían algo. OpenAI dice que contactó para ofrecer una publicación simultánea reconociéndoles la prioridad.

Buckmaster lo cuenta distinto. Dice que Sébastien Bubeck le ofreció elegir: publicar el resultado parcial y dejar que OpenAI anunciara el completo, o publicar y reclamar él el premio, a condición de confirmar que el modelo de OpenAI también lo había resuelto y de quitar a Alpöge de la lista de autores, por su vínculo con Anthropic. Buckmaster dice que se negó y que le preguntaron por qué querría arruinarse la carrera. OpenAI niega haber tocado ningún trabajo privado ni ningún log de Codex.

Yo no sé qué se dijo en esas llamadas y tú tampoco, y las disputas de prioridad son tan viejas como las matemáticas. Suelen ser aburridas: dos personas llegan casi a la vez, el registro lo ordena, todo el mundo se queda mosqueado durante una década.

La cláusula de la afiliación es lo que no consigo dejar pasar, y es justo la parte de la acusación que no tiene nada que ver con quién llegó antes. Una lista de autores no es un panel de patrocinadores. Es el registro de quién hizo el trabajo, y da la casualidad de que es el único artefacto de toda esta historia que ningún kernel de Lean nos va a verificar jamás. Pedir que se caiga un nombre por dónde cobra esa persona es otra categoría de petición distinta a "cítanos a nosotros también", y tratar ambas como intercambiables es como acabas con una literatura en la que nadie confía.

Respuestas y comprensión

Terence Tao calificó el trabajo de Buckmaster y Alpöge de logro notable, y a continuación soltó la frase que llevo días con ella dando vueltas: este año se ha producido un desacoplamiento rarísimo y sin precedentes entre obtener respuestas y obtener comprensión.

Y eso es exactamente lo que es una demostración de cien páginas verificada en Lean. Tienes un certificado de que el enunciado es cierto. Lo que no tienes automáticamente es aquello para lo que estaban las matemáticas: alguien capaz de contarte por qué los fluidos hacen esto, cuál es el mecanismo, qué más implica. Antes las dos cosas llegaban juntas, porque la única forma de conseguir el certificado era que hubiera humanos que lo entendieran lo bastante bien como para comprobarlo a mano. Ese acoplamiento ya no está. Nadie ha decidido qué lo sustituye.

Mientras tanto el Clay Institute no ha aceptado nada y sigue listando Navier–Stokes entre los problemas sin resolver. Sus reglas exigen que una solución pase dos años en una revista con revisión por pares y gane aceptación general en el campo antes siquiera de convocar un comité del premio. Martin Bridson declaró que el proceso de evaluación es deliberadamente pausado y será absolutamente riguroso, cosa que me encanta. Deliberadamente pausado es la postura correcta para la institución cuyo único trabajo es ser la palabra lenta, aburrida y definitiva.

OpenAI dice que no va a reclamar el millón de todas formas. Con el reloj de dos años por delante, el gesto sale más barato de lo que suena, pero sigue siendo lo correcto y quita de la mesa el incentivo más feo disponible.

Lo que yo me llevaría

Esta semana la verificación formal dejó de ser una curiosidad. Si tenías Lean y mathlib archivados en interesante, académico, no es mi problema: cien páginas de análisis de frontera pasaron de irrevisables a mecánicamente ciertas en menos de un día. Esa capacidad no se queda en matemáticas puras. Especificaciones de protocolo, reglas de consenso, primitivas criptográficas: todo aquello donde "lo revisamos con cuidado" es hoy el argumento de seguridad completo es candidato.

La lección más ancha: cuando automatizas la mitad comprobable de una revisión, presupuesta que la otra mitad va a subir mucho el volumen. Todo lo que se escondía cómodamente detrás de aún tenemos que verificar esto —atribución, propiedad, crédito, quién anuncia— se convierte en el calendario entero en cuanto verificar deja de llevar un año.

Y una práctica y pequeña, porque la vamos a necesitar bastante. Los próximos años, "una IA ha demostrado X" va a significar cualquier cosa entre un teorema verificado en Lean y una nota de prensa. Pregunta qué enunciado exacto. Pregunta si hay formalización. Pregunta quién más estaba ya trabajando en ello. Tres preguntas, y con eso se habría resuelto casi toda esta semana antes de empezar.