An AI System Proves an 18-Year-Old Quantum Conjecture, and a Computer Checks Every Step
A research system built by Physical Superintelligence, a laboratory known as PSI, has produced a proof of the Aaronson-Ambainis conjecture, a central open problem in quantum computing that had stood since 2008. PSI announced the result on Friday, saying that its internally developed system, running instances of a non-public Anthropic model on PSI's own infrastructure, had a complete proof during the third day of the run. The proof was then accepted by Lean, a proof assistant that checks every logical step by computer.