Estos días la comunidad matemática está revolucionada. El exdirector de ingeniería de Google DeepMind, David Budden, sorprendió a propios y extraños proclamando que había resuelto uno de los problemas del milenio: el de Navier–Stokes, utilizando una inteligencia artificial generativa (un LLM). Lo que parecía una hazaña histórica ha derivado, para muchos, en un caso de psicosis por IA.
El problema de Navier–Stokes
Los problemas del milenio son siete problemas matemáticos cuya resolución está premiada con un millón de dólares. A día de hoy, solo uno ha sido resuelto: la conjetura de Poincaré. Su autor, Grigori Perelman, rechazó tanto el premio como el reconocimiento institucional y se retiró de la vida académica.
El problema de Navier–Stokes trata de entender el comportamiento de los fluidos. Las ecuaciones que lo describen se usan habitualmente en simulaciones físicas, por ejemplo en cine o videojuegos. Pero el problema matemático es mucho más profundo: dado un estado inicial del fluido, ¿puede demostrarse que la solución existe para todo tiempo y que no aparecen singularidades (valores infinitos o comportamientos físicamente imposibles)?
David Budden, ahora CEO de una startup llamada PingYou, afirma haber resuelto este problema usando un LLM, y ha llegado incluso a apostar 10.000 dólares a que su demostración es correcta.
x.com/mhutter42/status/2001857421569032444
La comunidad matemática se da cuenta del pastel
La prueba presentada por Budden consistía en una formalización del problema y su supuesta solución en Lean, un asistente de pruebas matemáticas que permite verificar demostraciones formales. lean-lang.org
Sin embargo, para demostrar algo en Lean es necesario definir el problema con precisión absoluta. Y aquí surge el punto crítico: no existe todavía una formalización completa y aceptada del problema de Navier–Stokes del milenio. La comunidad matemática detectó rápidamente que la definición usada por Budden no correspondía al problema original, sino a una versión simplificada que ya había sido estudiada y resuelta décadas atrás.
En otras palabras: no se resolvió el problema de Navier–Stokes, sino un problema distinto que se le parecía superficialmente.
Cronología de la (incorrecta) solución
- El enunciado clásico del problema es deliberadamente conciso y deja implícitos muchos detalles.
- Budden pidió al LLM que formalizara el problema y demostrara existencia y regularidad usando Lean.
- El LLM identificó patrones similares a problemas ya resueltos presentes en sus datos de entrenamiento.
- Generó una formalización coherente y una prueba válida… pero de un problema más débil.
- Lean verificó correctamente esa demostración formal.
- Budden dio la prueba por válida al confiar en la validación formal, sin cuestionar la correspondencia con el problema original.
Aquí aparece el punto clave: un LLM no razona sobre la intención matemática del problema, sino que opera por reconocimiento estadístico de patrones lingüísticos. Cuando se enfrenta a un problema abierto, tiende a colapsar hacia el problema conocido más cercano, rellenando los huecos con hipótesis.
Algo similar ocurre en programación: un LLM puede generar código que compila y pasa tests, pero si también genera los tests, está dejando fuera precisamente aquello que no sabe comprobar. El famoso unknown unknown.
¿Psicosis por IA?
A pesar de las críticas de la comunidad matemática, Budden ha seguido defendiendo su postura. De hecho, ayer anunció en un estilo pasivo-agresivo que publicará la prueba en cinco entregas “al estilo MCU” (universo marvel).
Aquí el problema es confundir la validación formal de un sistema con la resolución de una pregunta matemática abierta.
En internet se ha especulado con que este caso podría encajar en lo que coloquialmente se denomina psicosis por IA. El término describe situaciones en las que la interacción con sistemas de IA contribuye a:
- Atribuir conciencia, intenciones o capacidades casi humanas a una IA.
- Reforzar ideas erróneas cuando la IA responde con seguridad y coherencia.
- Perder el juicio crítico y tratar salidas probabilísticas como verdades absolutas.
- Usar la IA como fuente principal de validación intelectual.
- Confundir simulación con comprensión real, especialmente en contextos complejos.
¿Estamos ante un caso de psicosis por IA?
¿Un sesgo de validación llevado al extremo?
¿O realmente alguien ha resuelto uno de los problemas del milenio?
Por ahora, la comunidad matemática sigue esperando pruebas reales. El desenlace, de momento, sigue abierto.
owiks 
tul 
Torrezzno 
rojo_separatista 
imparsifal 
