PSI presenta una prueba de la conjetura de Aaronson-Ambainis verificada por máquina

Physical Superintelligence anunció el 6 de noviembre de 2026 que un sistema de investigación interno, que ejecutaba instancias de un modelo no público de Anthropic, había encontrado una prueba de la conjetura de Aaronson-Ambainis, un problema de computación cuántica que permanecía sin resolver desde 2008.

El sistema produjo una prueba completa durante el tercer día de una ejecución en la propia infraestructura de PSI, y el asistente de pruebas Lean la aceptó. PSI asignó entonces al sistema problemas abiertos relacionados, y este mejoró el resultado dos veces antes de que Lean aceptara la versión final. El manuscrito y la formalización en Lean 4 son públicos.

Qué dice la conjetura sobre las aceleraciones cuánticas

La cuestión es cuándo las computadoras cuánticas pueden ser exponencialmente más rápidas que las máquinas clásicas. El algoritmo de factorización de Shor de 1994 depende de la estructura: su entrada contiene un patrón repetitivo que el algoritmo puede aprovechar. El resultado de PSI aborda el caso opuesto, el de las entradas aleatorias o carentes de estructura, en las que, por lo general, no existe tal patrón.

En el modelo de consultas, un algoritmo clásico lee un bit por consulta, mientras que una consulta cuántica puede distribuirse en superposición entre muchas posiciones de la entrada. La explicación de PSI vincula este modelo con los polinomios: después de T consultas cuánticas, la probabilidad de que el algoritmo responda «sí» es un polinomio acotado de los bits de entrada, de grado como máximo 2T. Por tanto, simular el algoritmo cuántico se convierte en una cuestión de estimar ese polinomio sin leer exponencialmente muchos bits de entrada.

En su artículo original, Scott Aaronson y Andris Ambainis conjeturaron que todo polinomio acotado de grado bajo tiene una variable muy influyente. Demostraron que, suponiendo cierta la conjetura, todo algoritmo cuántico de T consultas puede ser simulado en la mayoría de las entradas por un algoritmo clásico que realiza un número polinómico de consultas en T. La consecuencia es un crecimiento polinómico, en lugar de exponencial, del número de consultas clásicas para cualquier error de aproximación fijo y cualquier fracción de entradas excluidas; esto no descarta ventajas cuánticas exponenciales para problemas con una estructura adecuada.

Formalmente, el repositorio considera un polinomio real p de grado como máximo d, cuyos valores en el cubo discreto se encuentran entre 0 y 1. Si su varianza sobre una entrada aleatoria uniforme es al menos ε, alguna coordenada tiene una influencia de al menos (8√15 / (125π⁴)) · ε^(5/2) / d⁶ y, en consecuencia, de al menos (ε/d)⁷. La influencia es el cambio cuadrático esperado en p cuando se invierte el bit de esa coordenada.

Cómo se construyó y verificó la prueba

El argumento sigue un plan de Shachar Lovett y Jiapeng Zhang basado en certificados fraccionarios y conjuntos de nivel, pero sustituye una desigualdad que ese plan dejaba como conjetura por una nueva desigualdad para todos los pares. Un determinante genera una correspondencia biunívoca entre configuraciones de entrada. Según PSI, esta correspondencia va más allá de la correspondencia más débil del lema Butterfly de David Reimer, porque también limita la frecuencia con que las configuraciones emparejadas coinciden en cada coordenada, una cota necesaria para la nueva desigualdad.

El repositorio divide la prueba elemental en cuatro partes: deducir la desigualdad para todos los pares a partir del determinante y la biyección, integrarla sobre conjuntos de nivel, promediar sobre las coordenadas y establecer una cota por fila mediante una cota puntual de sensibilidad. En conjunto, estos pasos permiten obtener la cota explícita de influencia.

Según la auditoría registrada en el repositorio, el desarrollo formal no contiene marcadores de prueba pendientes ni axiomas añadidos. Las declaraciones se volvieron a ejecutar mediante el núcleo de Lean y lean4lean, una implementación independiente del verificador de tipos de Lean. En una ejecución aislada, un comparador que utiliza los núcleos de nanoda y Lean aceptó los cuatro teoremas finales; en una segunda máquina, aceptó una solución pequeña correcta y rechazó cuatro deliberadamente incorrectas.

Estas comprobaciones tienen límites explícitos. El lector aún debe confirmar que el enunciado formal coincide con la conjetura publicada. El artículo en lenguaje natural no está verificado por máquina, y el núcleo y el compilador de Lean, las definiciones de Mathlib y las máquinas utilizadas para la verificación siguen formando parte de la base de confianza.

Funciones humanas y revisión experta

David Turturean, miembro del personal técnico de PSI, desarrolló y ejecutó el sistema de investigación, delimitó el problema, indicó al modelo que preparara un primer borrador, revisó ese borrador y es responsable de la corrección del artículo. El repositorio declara que los modelos de IA produjeron los enunciados matemáticos, el primer borrador y la formalización en Lean. Jim Halverson auditó la prueba y Phiala Shanahan hizo comentarios sobre la formalización.

El anuncio se produce tras un artículo presentado el 19 de agosto de 2026 por Guy Blanc, Jordan Docter, Carmen Strassle y Li-Yang Tan. Estos autores habían resuelto la consecuencia relativa a la simulación clásica para algoritmos cuánticos paralelos, al demostrar que un algoritmo de t consultas y d rondas puede simularse en la mayoría de las entradas con t^(O(d²)) consultas clásicas. PSI afirma que los cuatro han estado leyendo la prueba completa, han aportado comentarios y están preparando una exposición más breve para especialistas.

En su evaluación publicada por PSI, los investigadores escribieron: «Es un resultado enorme. Resuelve una conjetura de hace décadas con importantes implicaciones para la naturaleza de los problemas que admiten aceleraciones cuánticas. La demostración se basa en varias líneas de investigación sobre el análisis de funciones booleanas y la combinatoria probabilística, y las amplía. Todo se integra de una manera casi mágica».

La prueba inmediata es inusualmente concreta: los núcleos independientes pueden volver a ejecutar el argumento codificado, mientras que los expertos aún deben confirmar que el enunciado codificado corresponde a la conjetura de Aaronson y Ambainis, y evaluar las partes del artículo que quedan fuera de Lean. Esta división determina qué queda establecido mediante las comprobaciones de la máquina y qué todavía requiere revisión matemática humana.