El 6 de noviembre de 2026, Physical Superintelligence (PSI) afirmó que su sistema interno, que usó instancias de un modelo no público de Anthropic, había producido una prueba de la conjetura de Aaronson–Ambainis aceptada por Lean. El repositorio público detalla qué proposición formaliza y señala que una persona debe confirmar que esa formulación expresa la conjetura pretendida. PSI publicó también el artículo y la formalización en Lean 4.
PSI dijo que el sistema completó una prueba al tercer día de ejecución y que Lean aceptó la versión final. La afirmación se refiere a una conjetura matemática sobre polinomios y consultas cuánticas; no a una demostración experimental.
Qué afirma el enunciado formal
El repositorio considera un polinomio real de grado como máximo d, cuyos valores están entre 0 y 1 en el cubo booleano {0,1}^N, y cuya varianza bajo entradas uniformes es al menos ε > 0. La varianza mide cuánto se dispersan sus valores cuando las entradas se eligen uniformemente.
La influencia de un bit mide cuánto cambia el valor del polinomio, en promedio, al invertir ese bit, con el cambio elevado al cuadrado. Para alguna coordenada, el repositorio afirma una cota de al menos (8√15/(125π⁴)) · ε^(5/2)/d⁶. También presenta la conjetura formalizada, a la que llama PrintedConjecture, con la cota (ε/d)^7.
La comprobación de una proposición formal y la confirmación de que esa proposición representa la conjetura original son dos tareas distintas.
Qué verifica Lean
Lean es un asistente de pruebas: comprueba que una conclusión se deriva de las definiciones y reglas escritas en su sistema lógico. El repositorio enumera cuatro declaraciones finales de teoremas y describe comprobaciones con el kernel de Lean y con lean4lean. También afirma que el desarrollo formal no contiene pasos pendientes ni axiomas añadidos.
Ese control verifica la derivación de la proposición formal. El propio repositorio indica que corresponde a los lectores confirmar que PrintedConjecture refleja la conjetura pretendida. Además, distingue la formalización del artículo legible por humanos, que no está comprobado íntegramente por máquina. El repositorio sitúa parte de la base de confianza en el kernel y el compilador de Lean, las definiciones de Mathlib y las máquinas que ejecutan las comprobaciones.
PSI dijo el 6 de noviembre que Guy Blanc, Jordan Docter, Carmen Strassle y Li-Yang Tan, de Stanford, estaban leyendo la prueba, habían enviado comentarios y preparaban una exposición más breve para especialistas.
Qué implica para las consultas cuánticas
En el modelo de complejidad de consultas, se cuenta cuántas veces un algoritmo accede a la entrada. PSI explica que la probabilidad de que un algoritmo cuántico responda «sí» tras T consultas puede representarse mediante un polinomio acotado de grado como máximo 2T.
La consecuencia que PSI atribuye al resultado se refiere a aproximar esa probabilidad con un número polinómico de lecturas clásicas de la entrada, para todos salvo una fracción pequeña de entradas aleatorias y con la tolerancia de error y la fracción fijadas. El resultado trata de consultas dentro de ese marco; no concluye que desaparezca toda ventaja cuántica ni establece el tiempo total de ejecución de cualquier tarea cuántica. La explicación de PSI vincula así el teorema con la simulación clásica de ciertos resultados en entradas aleatorias, no con una regla general sobre todos los algoritmos cuánticos.
