La propuesta de OpenAI para resolver el problema de Navier-Stokes abrió una discusión sobre cómo comprobar resultados matemáticos producidos con Inteligencia Artificial. La empresa anunció en septiembre una demostración obtenida con unos 10.000 agentes de IA, seguida de una verificación con Lean, un programa de comprobación matemática.
Un estudio difundido en octubre en arXiv, un repositorio de manuscritos científicos, por Alexander Bastounis, Fabian Circelli y Anders Hansen identificó diferencias entre argumentos del texto publicado y su versión formal. Comprobar esta última, advierten, no garantiza que la explicación escrita sea correcta.
El caso también provocó una controversia sobre la posible influencia de investigaciones inéditas. Son discusiones diferentes, una sobre la comprobación de la prueba y otra sobre el origen del avance y el reconocimiento del trabajo humano.
Qué busca resolver el problema de Navier-Stokes
Estas ecuaciones describen el movimiento de líquidos y gases, como agua y aire. Permiten estudiar desde la circulación sanguínea hasta el vuelo de aviones. Imaginemos un remolino inicialmente suave. La pregunta es si las ecuaciones siempre describirán su evolución sin valores que se disparen hasta el infinito.
Las ecuaciones surgieron en el siglo XIX. En 1934, Jean Leray demostró que existen soluciones en un sentido generalizado, pero quedó abierta la pregunta de si siempre mantienen su regularidad. En 2000, el Instituto Clay incorporó el desafío a los siete Problemas del Milenio.
OpenAI presentó un caso donde una fuerza externa suave, sin impulsos bruscos, actúa sobre el fluido y su velocidad crece sin límite en un tiempo finito, aunque la energía total permanece limitada. Esa singularidad marca un límite de la descripción matemática. Un líquido real no alcanza velocidad infinita.
Cómo los agentes encontraron la prueba y qué revisó Lean
Según OpenAI, grupos de agentes de IA exploraron distintas vías, consultaron material y ejecutaron código. El equipo humano redistribuyó recursos hacia Navier-Stokes tras un avance en las ecuaciones de Euler, un problema relacionado, y reunió resultados intermedios para orientar nuevos intentos.
La búsqueda tomó 88 horas. Después, GPT-6 Astra dedicó otras 17 a formalizar y verificar la demostración con Lean. El programa comprueba que los pasos respeten las reglas lógicas y los supuestos declarados. Revisar ese camino no exige conocer de antemano la respuesta ni repetir toda la búsqueda.
El estudio de Bastounis y sus colegas encontró pasajes donde Lean utiliza condiciones más exigentes o argumentos distintos del documento. Es como comprobar un cálculo y revisar, además, que corresponda a la pregunta original. Los autores cuestionan la fidelidad de la traducción, sin declarar incorrecta toda la prueba escrita.
En la otra controversia, el matemático Tristan Buckmaster planteó dudas sobre si el trabajo inédito que desarrollaba con Levent Alpöge, utilizando también Codex, pudo influir en OpenAI. Reconoció que desconocía si sus datos se usaron. La empresa negó acceder a su trabajo antes de su publicación y afirmó, tras investigar, que las instrucciones de Buckmaster a Codex de los dos meses anteriores no pudieron influir en el sistema, ni mediante entrenamiento.
“Una demostración brinda no solo certeza, sino también comprensión”, señala el Instituto Clay. Para considerar una solución para el premio exige publicación en un medio admisible, al menos dos años desde esa publicación y aceptación general de la comunidad matemática.
Fuentes
- OpenAI, propuesta de solución de Navier-Stokes
- Bastounis, Circelli y Hansen, estudio sobre diferencias entre texto y Lean
- Lean, documentación sobre comprobación de pruebas
- Instituto Clay, descripción del problema
- Instituto Clay, reglas de evaluación
- Tristan Buckmaster, declaración sobre su investigación y OpenAI
