Physical Superintelligence, known as PSI, a company building what it calls an AI-native physics research lab, said on Nov. 6 that a research system it built, running an unreleased Anthropic model, found a proof of the Aaronson-Ambainis conjecture. A conjecture is a math statement experts believe but nobody has proven. This one, from Scott Aaronson and Andris Ambainis and open since 2008, bears on when quantum computers can be exponentially faster than ordinary ones, meaning the gap keeps multiplying as problems get bigger.
Most of the dramatic speedups known for quantum computers rely on a hidden pattern in the problem. Peter Shor's 1994 quantum method for factoring large numbers works because the problem hides a repeating pattern, PSI explains. Researchers measure these speedups by how many times a computer must read its input, a long string of 0s and 1s. Whether quantum computers could be exponentially faster on random inputs, which almost never have such a pattern, was unknown.
Aaronson and Ambainis showed that if their statement about a kind of formula called a polynomial is true, the answer is no: on random inputs, an ordinary computer needs at most a fixed power of the quantum computer's number of reads, such as its square or cube, never exponentially more. With the proof, PSI says, an ordinary computer can predict how likely a quantum computer is to answer yes to a yes-or-no question on random inputs, up to a small error and for all but a small share of inputs. The number of reads the ordinary computer needs grows at most like a fixed power of the quantum computer's count, possibly a high one, but not exponentially. So, for yes-or-no questions, a quantum computer can save exponentially many reads only when the data has a rare pattern, as in factoring.
PSI says its system had a complete proof during the third day of its run, and Lean, a programming language in which a computer can check every step of a proof, accepted it. Working on related problems afterward, the system improved on the result twice, and Lean accepted the final version, PSI says. PSI has posted the paper and the Lean code, and says two separately built checking programs re-checked the code. The paper, written for human readers, is not computer-checked.
A computer check shows a proof is right only for the problem as it was typed in. PSI says a reader needs to check just one definition in the code to confirm that the typed version matches the conjecture.
In August, four Stanford University researchers proved what the conjecture predicts, no exponential quantum edge on random inputs, for one special case: quantum programs that read their input in a fixed number of parallel rounds. PSI says they have been reading its proof of the full conjecture, have sent comments and are writing a shorter explanation for experts. In a message PSI quotes in its post, they called it "a huge result" and wrote: "Everything is brought together in a rather magical way."
PSI says the math statements, the first draft of the paper and the Lean version were all produced by AI models. David Turturean, the PSI staff member who built the research system, reviewed the paper and is responsible for its correctness, PSI says. Jim Halverson, a PSI adviser, audited the proof. PSI has not named the Anthropic model it used, and Anthropic did not respond to a request for comment, according to a news report.