Startup Physical Superintelligence (PSI) says its AI system, built on an unreleased Anthropic model, has proved the Aaronson-Ambainis conjecture on the limits of quantum speedups in data queries, and Lean has verified the proof

Startup Physical Superintelligence (PSI) says its AI system, built on an unreleased Anthropic model, has proved the Aaronson-Ambainis conjecture on the limits of quantum speedups in data queries, and Lean has verified the proof

On November 6, PSI researcher David Turturean published the paper and code. The conjecture implies that, for problems with a yes-or-no answer, a quantum algorithm cannot use exponentially fewer data queries than a classical computer on almost all inputs.

Exponential quantum speedups usually rely on structure hidden in the data: Shor's algorithm factors integers because a quantum computer can find a repeating period in the problem. The speedup is measured in queries to a string of zeros and ones: a classical query reads one bit, while a quantum query can access many positions at once. Whether such a speedup was possible on a random string with little structure remained unknown.

Quantum computing researchers Scott Aaronson and Andris Ambainis posed this question. In 2009, they reduced it to an unproved conjecture about polynomials. The probability that a quantum algorithm making T queries answers “yes” is a polynomial in the input bits, with values from 0 to 1 and degree (the largest number of bits multiplied together) at most 2T. To approximate this probability on almost all inputs, a classical computer that knows the polynomial reads the bits one at a time, choosing an influential bit: one whose value, when changed, substantially changes the polynomial's value. Once the unread bits have little effect, it uses the polynomial's average value as the probability of a “yes” answer.

The conjecture states that an influential bit exists regardless of how many bits the input contains. The paper proves the following bound: if the values of a polynomial of degree at most d vary substantially (with variance at least ε), at least one bit has influence of at least (ε/d)⁷. The classical computer needs a number of queries on the order of the total influence of all bits (at most 2T) divided by the guaranteed influence of a single bit. Previous influence guarantees decreased exponentially with degree, which would require exponentially many queries; an exponent of 7 gives a query count on the order of T⁸ for a fixed accuracy and fraction of exceptions.

According to PSI's disclosure, the mathematical claims, paper draft and formal proof in Lean were produced by AI, while Turturean set the task and takes responsibility for the paper. The first proof, with an exponent of 22, emerged on the system's third day of work. Turturean writes: “The model proposed a series of important lemmas that remained unproved until the last one was finally proved, and then everything simply fell into place.” The system then improved the bound twice, reducing the exponent to 11 and then to 7.

The proof follows an approach proposed by researchers Shachar Lovett and Jiapeng Zhang. One inequality in that approach remained conjectural and, according to the paper, is false in its original form. The system proposed and proved a new inequality to replace it.

According to PSI, Lean verified every step of all three versions. Readers can check the Lean statement of the conjecture themselves: it fits into a single definition in a file that uses only the Mathlib mathematics library. PSI says that four Stanford University researchers who proved a special case of this consequence are reading the proof.

Reflecting on the proof, Turturean writes that it “still feels a little alien” and that “literally everyone needs to work out” what to do when such central problems can be solved relatively quickly.