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.
The conjecture, posed by Scott Aaronson and Andris Ambainis, asks a simple question: when can a quantum computer be exponentially faster than an ordinary computer? Famous quantum speedups, such as Peter Shor's 1994 factoring algorithm, depend on structure, a rare repeating pattern hidden in the input. Aaronson and Ambainis showed that if a statement about polynomials is true, then no such exponential advantage exists on random inputs, which almost never carry that kind of structure. Proving the polynomial statement is what PSI says its system has now done.
The practical meaning is measured in looks at the input. Each look lets an ordinary computer read one bit, while a quantum look can be spread across many positions at once. Because a quantum algorithm's probability of answering yes is a polynomial in the input bits, an ordinary computer can imitate it by predicting that polynomial's value while reading only a few influential bits. The new proof guarantees that some bit always has influence at least a fixed power of the polynomial's variation divided by its degree, with the constant in PSI's bound about 0.0025. In plain terms, the ordinary computer needs at most a polynomial number of extra looks, not an exponential number, for all but a small fraction of inputs.
PSI says the work followed a plan laid out by Shachar Lovett and Jiapeng Zhang, who had left one key inequality unproved. The new proof replaces that step with a different inequality, established by pairing up input settings one to one with the help of a determinant, and it also draws on earlier work by David Reimer and others. After the first complete proof, PSI pointed the system at related problems, and it improved the result twice, with Lean accepting the final version as well. David Turturean, a member of PSI's technical staff, led the work, built the research system, and is responsible for the paper's correctness. Jim Halverson audited the proof, and Phiala Shanahan commented on the Lean formalization.
There is encouraging outside interest, and there are clear limits. In August, a Stanford team of Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan settled the conjecture's prediction in a special case. That group has since read the full proof, sent comments, and is writing a shorter exposition for experts, calling it a huge result that resolves a decades-old question. At the same time, a machine check is not the whole story. Lean verifies the formal statement it is given, so human mathematicians still have to confirm that the formal statement matches the conjecture as Aaronson and Ambainis originally meant it, and the readable paper itself is not machine-checked.
Even with those caveats, the announcement marks a notable moment for AI-assisted research. A system built around a model that the public cannot yet use did not merely suggest an approach or check a calculation. According to PSI, it assembled a complete, machine-verified argument for a problem that specialists had worked on for eighteen years, and it then strengthened its own result. Quantum computing still has plenty of mysteries. After Friday, it has one fewer.