Physical Superintelligence (PSI) anunció el 6 de noviembre de 2026 que un sistema interno de investigación con IA, que ejecutaba instancias de un modelo no público de Anthropic, encontró una prueba de la conjetura de Aaronson-Ambainis, una cuestión de computación cuántica abierta desde 2008. El sistema produjo una prueba completa durante el tercer día de una ejecución en la propia infraestructura de PSI, y Lean —un asistente de pruebas que verifica por máquina cada paso de un argumento matemático— la aceptó. PSI puso luego el sistema a trabajar en problemas abiertos relacionados, mejoró el resultado dos veces y Lean aceptó la versión final. El manuscrito y la formalización en Lean 4 son públicos.

La conjetura pregunta cuándo los ordenadores cuánticos pueden ser exponencialmente más rápidos que las máquinas clásicas. Si la prueba de PSI se sostiene, un ordenador ordinario puede estimar la probabilidad de que un algoritmo cuántico responda que sí, en la mayoría de las entradas y con un margen de error fijo, sin leer la entrada exponencialmente más veces; en otras palabras, las aceleraciones cuánticas exponenciales exigen patrones o estructura especiales en el problema, un límite sospechado desde hace tiempo pero nunca demostrado. PSI dice que su prueba sigue un plan trazado por Shachar Lovett y Jiapeng Zhang, que habían dejado sin demostrar una desigualdad clave; el nuevo artículo demuestra una desigualdad sustituta y da un límite explícito.

Lo que hace la afirmación más difícil de descartar que un titular típico de «la IA resolvió matemáticas» es la verificación. El repositorio de PSI dice que el desarrollo formal no contiene marcadores de prueba ni axiomas añadidos, y que sus declaraciones se reprodujeron a través del núcleo de Lean y de lean4lean, una implementación independiente del verificador de tipos de Lean. En una ejecución aislada, un comparador que usaba los núcleos de nanoda y Lean aceptó los cuatro teoremas finales, y en una segunda máquina aceptó una solución pequeña correcta y rechazó cuatro deliberadamente erróneas. David Turturean, miembro del personal técnico de PSI, construyó el sistema de investigación, delimitó el problema, pidió al modelo que empaquetara un primer borrador, revisó ese borrador y es responsable de la corrección del artículo; el asesor de PSI Jim Halverson auditó la prueba, y el repositorio revela que los modelos de IA produjeron los enunciados matemáticos, el primer borrador y la formalización en Lean.

Las advertencias son reales y PSI las expone por sí misma. El resultado no está revisado por pares: la prueba aún no ha pasado la revisión de una revista, y los expertos humanos todavía tienen que confirmar que el enunciado formal codificado en Lean coincide con la conjetura tal como la entendieron Aaronson y Ambainis; el artículo legible por humanos no está verificado por máquina. Cuatro investigadores de Stanford que resolvieron un caso especial en agosto de 2026 están leyendo la prueba y escribiendo una versión más corta para expertos. Hay que tratarlo como una afirmación de empresa con un artefacto comprobable, no como un veredicto de revista, pero es llamativa: llega tras la publicación por OpenAI de 722 manuscritos de matemáticas escritos por IA en octubre, y es la evidencia más sólida hasta ahora de que los sistemas de IA están pasando de ayudar con las pruebas a producirlas.

Fuentes