Conjetura de Aaronson-Ambainis: una IA demostró en tres días un enigma cuántico de 18 años

El 6 de noviembre, una pequeña empresa llamada Physical Superintelligence (PSI) anunció algo que hace una década habría sonado a ciencia ficción: un sistema de investigación de IA, que ejecuta un modelo no público de Anthropic, había demostrado la conjetura de Aaronson-Ambainis, un problema abierto central de la teoría de la complejidad cuántica que llevaba sin resolverse desde 2008. El sistema tenía una demostración completa al tercer día de ejecución. Lean, el asistente de demostración que verifica cada paso lógico por máquina, la aceptó. PSI puso entonces el sistema a trabajar en problemas relacionados, mejoró el resultado dos veces y publicó tanto el artículo como la formalización pública en Lean, para que cualquiera pueda volver a verificar el trabajo.

Para entender por qué importa, empecemos por aquello en lo que los ordenadores cuánticos son realmente buenos. En 1994, Peter Shor encontró un algoritmo cuántico que factoriza números grandes mucho más rápido que cualquier método clásico conocido. Pero la aceleración de Shor depende de un don poco común: el problema esconde un patrón repetitivo, y el ordenador cuántico encuentra con qué frecuencia se repite. La mayoría de las aceleraciones cuánticas espectaculares que se conocen funcionan igual. Explotan la estructura.

Scott Aaronson y Andris Ambainis plantearon la pregunta incómoda: ¿qué pasa con las entradas aleatorias, que casi nunca tienen esa estructura? ¿Puede un ordenador cuántico responder una pregunta de sí o no sobre una cadena aleatoria leyendo los bits exponencialmente menos veces que un ordenador corriente? Plantearon una conjetura sobre polinomios —matemática pura— y demostraron que, si es cierta, la respuesta es no: con entradas aleatorias, los ordenadores cuánticos son como mucho polinómicamente más rápidos. La conjetura se convirtió en uno de los problemas abiertos centrales de la teoría de la complejidad cuántica, y en agosto de 2026 un grupo de Stanford la demostró para un caso especial: algoritmos cuánticos que leen su entrada en un número fijo de rondas paralelas.

La demostración de PSI sigue un plan trazado por Shachar Lovett y Jiapeng Zhang, sustituyendo una desigualdad que su plan dejaba como conjetura por una nueva desigualdad demostrada en el manuscrito, mediante un argumento de emparejamiento basado en el lema de la mariposa de David Reimer y en resultados de varios otros grupos. El humano implicado, David Turturean de PSI, construyó el sistema de investigación, delimitó el problema, lo ejecutó y asume la responsabilidad de la corrección del artículo. El asesor Jim Halverson auditó la demostración. El grupo de Stanford que demostró el caso especial ha estado leyendo la demostración completa, envió comentarios y está escribiendo una exposición más breve para expertos. Su veredicto hasta ahora: «Es un resultado enorme».

Esa es la forma correcta de leer esta historia: no como una coronación, sino como una afirmación con un artefacto verificable. La aceptación de Lean es un listón alto: una máquina ha verificado cada paso del argumento. Lo que Lean no puede verificar es si el enunciado formal es el enunciado que realmente interesa a los matemáticos, o si la formalización introduce de contrabando una suposición oculta. Ese es el trabajo de los expertos humanos, y todavía está pendiente. La revisión por pares no ha ocurrido. El modelo que encontró la demostración no es público, así que nadie puede volver a ejecutar el descubrimiento en sí, solo inspeccionar lo que produjo.

Y ahí es donde la semana en la que cayó este anuncio se convierte en la verdadera historia. La demostración de PSI no es un hecho aislado. En octubre, OpenAI publicó 722 manuscritos matemáticos escritos por IA, incluidas supuestas demostraciones de la hipótesis cuasi-Riemann, la conjetura de los juegos únicos y la conjetura de Hodge para una clase especial de formas. En septiembre, un artículo en The Quarterly Journal of Mathematics informó de que un sistema de IA había encontrado la idea clave que convertía resultados condicionales sobre k-diferenciales en teoremas incondicionales, con el lema crucial demostrado formalmente en Lean. Axiom ha formalizado el Stacks Project, de unas 7.500 páginas —unos 16 millones de líneas—, haciendo que un enorme cuerpo de geometría algebraica sea verificable por máquina. El patrón ya es inconfundible: la IA propone y Lean dispone. El cuello de botella se ha trasladado de encontrar demostraciones a verificarlas, y en la verificación el ritmo lo siguen marcando los humanos.

Ese cambio es lo que estoy observando. Si la exposición de Stanford llega limpia y ningún grupo rival encuentra un hueco, la demostración de Aaronson-Ambainis se convertirá en el segundo gran resultado atribuido a la IA en un mes que sobrevive al escrutinio experto, y la pregunta dejará de ser si la IA puede hacer matemáticas de frontera para convertirse en lo rápido que el proceso de verificación puede seguirle el ritmo. Mi predicción: para el 31 de diciembre de 2027, esta demostración habrá sido confirmada públicamente por matemáticos independientes, a través de la exposición del grupo de Stanford, una publicación revisada por pares o una confirmación pública equivalente de expertos, sin que se encuentre ningún fallo material. Le doy un 65%: el listón mecánico ya está superado, los expertos adecuados ya están implicados, pero la confirmación humana no es un trámite, y una sola discrepancia de definición aún puede hundir una demostración verificada por Lean.