Un sistema automatizado resuelve en tres días la conjetura cuántica de Aaronson-Ambainis
La startup de investigación física PSI utiliza modelos de Anthropic y la verificación con Lean para abordar una cuestión computacional de 18 años.
Traducido automáticamente del original en inglés Leer el original
Un sistema de investigación computacional ha generado una prueba matemática formal de la conjetura de Aaronson-Ambainis, un problema abierto de hace 18 años sobre los límites de la computación cuántica. La empresa de investigación física PSI anunció que su plataforma automatizada produjo la verificación en tres días, empleando inteligencia artificial para abordar cuándo las máquinas convencionales pueden aproximar algoritmos cuánticos.
Una limitación de 18 años sobre la ventaja cuántica
Propuesta por primera vez en 2008, la conjetura de Aaronson-Ambainis explora los límites exactos en los que los procesadores cuánticos mantienen una ventaja de velocidad exponencial sobre las arquitecturas digitales convencionales. Según informa Interesting Engineering, la conjetura se centra en si los algoritmos cuánticos que presentan una estructura matemática específica pueden ser simulados por hardware clásico con solo una sobrecarga polinómica. Cuando las máquinas clásicas simulan procesos sobre entradas elegidas al azar dentro de límites polinómicos, la aparente brecha operativa se reduce de forma significativa. Los procedimientos especializados establecidos, como el algoritmo de Shor para factorizar números enteros, no se ven afectados por la conjetura, ya que la cuestión matemática aborda un subconjunto distinto de cómputos cuánticos.
Automatizar la prueba formal con Lean
Para abordar la conjetura, el investigador David Turturean dirigió el trabajo en PSI, desarrollando el flujo de trabajo automatizado de investigación, formulando el problema computacional y supervisando la ejecución. El sistema se ejecutó en la infraestructura interna de PSI, utilizando un modelo de inteligencia artificial privado y no público desarrollado por Anthropic. Durante la prueba, la plataforma produjo enunciados formales que se cargaron directamente en Lean, un asistente interactivo para pruebas diseñado para verificar si las secuencias lógicas siguen estrictamente determinados axiomas matemáticos. El sistema revisó después el argumento en dos ocasiones, generando un resultado final que Lean aceptó sin discrepancias lógicas.
Verificación independiente y revisión académica
La comprobación formal del código garantiza la consistencia interna, pero los matemáticos aún deben establecer que el teorema traducido coincide con la proposición original de 2008. El físico Jim Halverson auditó la estructura de la prueba, mientras que la física teórica del MIT Phiala Shanahan examinó la formalización creada en Lean. En paralelo, un equipo de investigación matemática de la Universidad de Stanford, formado por Guy Blanc, Jordan Docter, Carmen Strassle y Li-Yang Tan, comenzó a evaluar el resultado. El grupo de Stanford, que ya había demostrado un caso especial de la conjetura de Aaronson-Ambainis en agosto de 2026, está redactando un artículo técnico condensado para explicar los hallazgos de PSI a la comunidad científica en general.
Próximos pasos para el descubrimiento científico automatizado
El proyecto representa una demostración práctica de innovación en matemáticas asistidas por máquina de PSI, una startup presentada públicamente en septiembre de 2026 para construir motores de descubrimiento autónomos. Si bien Lean proporciona una validación programática de la lógica, la prueba aún no ha completado la revisión por pares estándar en la comunidad académica de la física. La futura difusión y revisión por parte de teóricos externos determinará si la prueba resuelve por completo la conjetura de Aaronson-Ambainis.
