Investigación
OpenAI reclama una solución al problema de Navier-Stokes con 10.000 agentes y abre una disputa por la autoría
OpenAI anunció que un despliegue masivo de agentes de IA produjo en 88 horas una propuesta de solución al problema de Navier-Stokes, uno de los siete Millennium Prize Problems (Problemas del Milenio) dotados con un millón de dólares. El anuncio llegó acompañado de formalizaciones en Lean y de una polémica inmediata sobre el crédito y el papel de los matemáticos humanos que ya trabajaban en el mismo terreno.
Recibe el resumen diario de IA
Cada mañana, lo esencial de la inteligencia artificial en tu correo, sin humo. Al día con la IA.
Al suscribirte aceptas recibir el newsletter de AI Informator. Puedes darte de baja cuando quieras.
En resumen
- OpenAI afirma haber empleado unos 10.000 agentes coordinados durante 88 horas para generar una propuesta de demostración sobre Navier-Stokes.
- El coste declarado del operativo ronda los 22 millones de dólares y unos 300.000 millones de tokens de salida.
- La compañía publicó las formalizaciones en Lean de Navier-Stokes y Euler en un repositorio público de GitHub para permitir su verificación.
- El matemático Tristan Buckmaster difundió una declaración pública sobre la cronología de su propia investigación, abriendo una disputa sobre la atribución del avance.
El problema que lleva casi un siglo resistiéndose
Las ecuaciones de Navier-Stokes describen el movimiento de fluidos viscosos: desde el agua que se agita en una taza hasta las corrientes atmosféricas. La pregunta abierta, formulada por el Clay Mathematics Institute como uno de sus Problemas del Milenio, es si esas ecuaciones admiten siempre soluciones suaves o si pueden desarrollar una singularidad, un punto donde las magnitudes se disparan hacia el infinito y el modelo deja de tener sentido.
Demostrar la existencia de singularidades en tiempo finito, o descartarla, tiene consecuencias que van mucho más allá de las matemáticas puras: afecta a la fiabilidad de la simulación numérica en aeronáutica, meteorología y oceanografía. Por eso la comunidad matemática trata cualquier reclamación en este terreno con extremada cautela y exige verificación independiente antes de dar nada por cerrado.
La verificación formal es el punto clave del anuncio
El elemento más comprobable del anuncio no es el resultado en sí, sino que OpenAI publicó formalizaciones en Lean, un demostrador asistido por ordenador (proof assistant) que verifica mecánicamente cada paso lógico de una demostración. Una prueba que compila en Lean no depende de la confianza en quien la escribió: el propio sistema rechaza cualquier salto injustificado.
Esa es la diferencia sustancial frente a episodios anteriores de supuestos avances matemáticos generados por modelos de lenguaje. El repositorio NavierStokesAndEuler permite a terceros ejecutar la verificación por su cuenta. Hasta que la comunidad complete ese escrutinio y el Clay Mathematics Institute se pronuncie, la propuesta sigue siendo eso: una propuesta pendiente de validación.
La disputa por la autoría revela un problema estructural
Tristan Buckmaster, especialista reconocido en dinámica de fluidos y singularidades, llevaba tiempo trabajando en la misma dirección y publicó una declaración detallando la cronología de su investigación. El desacuerdo gira en torno a qué parte del trabajo previo alimentó el resultado, en qué medida las líneas de ataque ya publicadas orientaron la búsqueda automatizada y cómo debe repartirse el crédito.
El caso expone una tensión que la comunidad científica aún no ha resuelto: cuando un sistema automatizado escala una idea humana previa hasta completarla, no existe una convención clara de autoría. Las normas de coautoría de las revistas científicas fueron diseñadas para personas, y ninguna contempla el estatus de una infraestructura de cómputo que consume millones de dólares en una semana.
El coste marca el verdadero límite de este enfoque
Los 22 millones de dólares y los 300.000 millones de tokens declarados sitúan este experimento fuera del alcance de cualquier departamento universitario. La estrategia consiste esencialmente en fuerza bruta dirigida: lanzar miles de agentes explorando ramas del espacio de demostraciones en paralelo, filtrando después lo que sobrevive a la verificación formal.
Ese modelo es reproducible solo por un puñado de laboratorios con acceso a cómputo a esa escala, lo que introduce una asimetría inquietante en la investigación matemática. Si los grandes resultados pasan a depender del presupuesto de GPU disponible, la frontera del conocimiento se desplaza hacia quien puede pagarla, no necesariamente hacia quien tiene la mejor idea.
Conclusión
Conviene separar dos cosas que el anuncio mezcla. La primera es técnica y verificable: existen formalizaciones en Lean publicadas que cualquiera puede comprobar, y ese es un estándar de rigor muy superior al de las demostraciones en lenguaje natural que los modelos venían produciendo. La segunda es institucional y está sin resolver: cómo se atribuye el mérito, cómo se reconoce el trabajo humano previo y qué significa investigar cuando el factor limitante es el presupuesto de cómputo. El resultado matemático se validará o se caerá en las próximas semanas mediante el escrutinio de la comunidad. La pregunta sobre quién firma los descubrimientos de la próxima década tardará bastante más en responderse.
Fuentes primarias
Recibe el resumen diario de IA
Cada mañana, lo esencial de la inteligencia artificial en tu correo, sin humo. Al día con la IA.
Al suscribirte aceptas recibir el newsletter de AI Informator. Puedes darte de baja cuando quieras.
Comentarios