El 8 de septiembre OpenAI publicó un preprint, un anuncio y un repositorio público en Lean 4 en los que afirma que un modelo interno, no publicado, produjo una prueba sobre las ecuaciones de Navier–Stokes en tres dimensiones, uno de los siete problemas del milenio del Clay Mathematics Institute. La afirmación tiene un alcance preciso, y a 11 de septiembre ningún matemático ni organismo independiente había publicado una verificación.
Qué afirma la prueba
El enunciado oficial, escrito por Charles Fefferman, pide demostrar una cualquiera de cuatro afirmaciones. Dos de ellas, (A) y (B), probarían que las soluciones suaves existen para siempre cuando no actúa ninguna fuerza externa sobre el fluido. Las otras dos, (C) y (D), probarían lo contrario: que hay condiciones iniciales suaves y una fuerza externa suave para las que no existe una solución bien comportada durante todo el tiempo.
OpenAI afirma haber probado (C) y (D). Su construcción dice que, para cualquier viscosidad positiva, hay datos iniciales suaves en reposo y una fuerza suave con los que la velocidad se vuelve ilimitada en un tiempo finito mientras la energía se mantiene acotada. Tal como está escrito el problema, demostrar una de las cuatro afirmaciones cuenta como resolverlo. No toca (A) y (B), el caso sin fuerza, y si una construcción con fuerza externa es lo que el problema quería capturar forma parte del debate actual. La propia tarjeta de la portada de OpenAI dice que el modelo «propone» una solución.
Cómo se obtuvo, según OpenAI
Según OpenAI, el modelo que encontró la prueba es interno y más capaz que GPT-6 Astra. Funcionó como unos 10.000 agentes simultáneos y llegó al resultado unas 88 horas después de arrancar; después, GPT-6 Astra tardó otras 17 horas en formalizarlo y comprobarlo en Lean. Son cifras de OpenAI, y no se ha publicado ningún método de evaluación del modelo.
Lo que muestra la formalización en Lean, y lo que no
El repositorio no deja ningún paso sin demostrar, usa sólo los axiomas estándar de Lean e incluye configuraciones para que terceros vuelvan a comprobar las pruebas con Comparator, una herramienta que confirma que una prueba demuestra exactamente el teorema enunciado. Los enunciados de partida se adaptaron del proyecto Formal Conjectures de Google DeepMind. Quedan dos límites: una comprobación automática confirma la prueba del enunciado en Lean, no que ese enunciado recoja lo que los matemáticos entienden por el problema, y los metadatos del propio repositorio declaran su revisión como «autoevaluada».
Dónde están el premio y la comunidad
La página del Clay Institute sigue mostrando el problema como abierto. Sus reglas exigen la publicación en una revista con revisión, al menos dos años y la aceptación general de la comunidad matemática antes de estudiar un premio, y OpenAI dice que no piensa reclamarlo. La Sociedad Matemática Europea calificó el anuncio de «hito en la historia de las matemáticas», porque «un gran problema abierto quizá se haya resuelto por fin», y señaló que el trabajo parte de una estrategia ya propuesta por otros matemáticos.
Una disputa de prioridad al lado
Las matemáticas llegan con un conflicto. Tristan Buckmaster, de la NYU, y Levent Alpöge publicaron sus propios resultados con fuerza suave para ecuaciones relacionadas horas antes del anuncio de OpenAI. En un comunicado público, Buckmaster describe sus contactos con OpenAI en los días previos, incluidas dos propuestas de publicación conjunta, y escribe: «No he visto la prueba de OpenAI. No sé qué hizo su modelo, ni cómo». OpenAI dice que contactó con los dos sólo después de terminar su propio trabajo, y que les ofreció una publicación conjunta y el reconocimiento de su prioridad.
Qué dar por cerrado
Está cerrado lo que OpenAI publicó y afirma, qué enunciados busca y que su compilación en Lean no deja huecos. No lo está si la prueba es correcta ni si los enunciados en Lean coinciden con el problema tal como lo lee la comunidad. El titular honesto es una afirmación en revisión, y lo que hay que vigilar son las primeras comprobaciones independientes.
Lecturas relacionadas
- Descripción oficial del problema, de Charles Fefferman — Clay Mathematics Institute
- Repositorio NavierStokesAndEuler — OpenAI
- GPT-6 Astra llega como producto — IA al Día