PSI: un sistema de IA halla una demostración en Lean de la conjetura de Aaronson-Ambainis
Physical Superintelligence anuncia que un sistema de investigación interno, apoyado en un modelo no público de Anthropic, ha hallado una demostración de la conjetura de Aaronson-Ambainis (2008), aceptada por Lean 4. El manuscrito y la formalización ya son públicos.
Physical Superintelligence (PSI) anunció el 6 de noviembre de 2026 que un sistema de investigación interno, impulsado por instancias de un modelo no público de Anthropic, ha encontrado una demostración de la conjetura de Aaronson-Ambainis, abierta desde 2008. Según el laboratorio, Lean aceptó una demostración completa al tercer día del proceso y, posteriormente, dos mejoras. El manuscrito y la formalización en Lean 4 son públicos.
Qué dice la conjetura
Scott Aaronson y Andris Ambainis se preguntaban si un ordenador cuántico puede responder a una pregunta de sí/no sobre una cadena aleatoria con exponencialmente menos consultas que un ordenador clásico. La mayoría de las aceleraciones espectaculares conocidas (como el algoritmo de Shor) se basan en una estructura poco habitual en la entrada. Su conjetura de matemática pura, de ser cierta, implica que, en ausencia de dicha estructura, el sobrecoste clásico sigue siendo como máximo polinomial respecto al número de consultas cuánticas.
En la práctica, tras T consultas, la probabilidad de que un algoritmo cuántico responda «sí» es un polinomio de grado como máximo 2T con valores en [0, 1]. La conjetura sostiene que un polinomio de este tipo, si varía lo suficiente, siempre tiene una variable con una influencia bastante grande, lo que permite a un ordenador clásico imitar la predicción examinando únicamente unos pocos bits.
Qué publica PSI
La página de investigación y el repositorio de GitHub describen una demostración que sigue una estrategia planteada por Lovett y Zhang, sustituyendo una desigualdad que ellos habían dejado abierta. El archivo README asegura que contiene cuatro teoremas en Lean sin marcadores de posición ni axiomas añadidos, verificados de nuevo por dos implementaciones del núcleo de Lean (versiones 4.33.0 / Mathlib v4.33.0, licencia Apache 2.0). David Turturean dirigió el trabajo; Jim Halverson auditó la demostración; Phiala Shanahan comentó la formalización.
En agosto de 2026, cuatro investigadores de Stanford (Blanc, Docter, Strassle, Tan) ya habían resuelto un caso particular. PSI señala que ahora están leyendo la demostración completa y preparando una exposición más breve; el laboratorio cita comentarios elogiosos de su parte.
Límites que conviene tener presentes
El repositorio deja en manos del lector la tarea de comprobar que el enunciado en Lean PrintedConjecture se corresponde fielmente con la conjetura impresa. Un teorema mejorado se fundamenta en una hipótesis de Agarwal y Ben-David no formalizada aquí. El artículo redactado en prosa no está verificado por máquina. El modelo de Anthropic no tiene nombre ni es público: se puede inspeccionar el resultado, pero no reproducir el proceso de descubrimiento. Al cierre de esta edición, no constaba ninguna reacción pública de Aaronson o Ambainis.
Nuestro análisis
La señal clave no es que «un modelo haya inventado la teoría de números», sino que un sistema de investigación vinculado a un verificador formal puede producir hoy un artefacto auditable sobre un problema abierto desde hace dieciocho años. La máquina propone, Lean valida una parte del trabajo y el ser humano sigue siendo responsable de velar por la correspondencia entre el enunciado formalizado y la conjetura original. Mientras esa fidelidad y la revisión por pares no se hayan resuelto, el enfoque adecuado es tratar el repositorio como una demostración candidata verificada por máquina, y no como un teorema ya asentado en el canon.
Fuentes
- PSI — A proof of the Aaronson-Ambainis conjecture (6 de noviembre de 2026) Fuente primaria
- GitHub — physical-superintelligence/aaronson-ambainis (artículo + Lean 4) Fuente primaria
- Aaronson & Ambainis — The Need for Structure in Quantum Speedups (arXiv:0911.0996) Fuente primaria — Enunciado original de la conjetura
Una fuente primaria procede directamente de la empresa, el laboratorio o la organización implicados. Una fuente secundaria recoge la información sin ser su autora: la señalamos como tal. ¿Has visto un error? Consulta nuestra política de correcciones.
