On 6 November Physical Superintelligence (PSI) published a press release on its website and a manuscript in its GitHub repository. Both state that a conjecture by Scott Aaronson and Andris Ambainis has been proved. PSI said the conjecture had been open since 2008.

The manuscript states that AI models produced its mathematical statements. David Turturean of PSI defined the problem and built the harness, a program that gives the model tools and runs its work steps. The harness ran several instances of an unreleased Anthropic model. The instances searched for earlier ideas, proposed and tested new ones, and monitored the work of other instances. PSI said the proof was complete on the third day of the run.

A model also wrote the first draft of the manuscript. Turturean reports reviewing and editing the draft and taking responsibility for its correctness.

What the result says about quantum computers

The input is a long string of zeros and ones. The query model counts how many times an algorithm reads it. It was already known that after T queries, the probability that a quantum algorithm answers ‘yes’ is a polynomial in the input bits. The polynomial has degree at most 2T and takes values between zero and one.

The conjecture states that such a polynomial has an influential bit unless its value is constant. A bit’s influence is the mean, over all inputs, of the squared change in the polynomial’s value when the bit is flipped. The manuscript states that some bit has influence of at least (ε/d)⁷, where d is the polynomial’s degree and ε a lower bound on its variance. Earlier general lower bounds weakened exponentially as the degree grew.

By an earlier result of Aaronson and Ambainis, a classical algorithm can therefore read influential bits one at a time. The manuscript says such an algorithm estimates the quantum algorithm’s ‘yes’ probability to within error ε on all but a δ fraction of inputs, using at most (4T)⁸ ε⁻¹⁴ δ⁻⁸ queries. The number of queries grows polynomially, not exponentially.

The result does not cover structured inputs. The manuscript states that a quantum speedup larger than polynomial in the query model requires structure, such as a guarantee about what the input looks like. PSI said Shor’s factoring algorithm, for example, relies on such structure.

The proof and how it was checked

The proof follows a plan by Shachar Lovett and Jiapeng Zhang but replaces the inequality they left as a conjecture with a new one. The proof of the new inequality pairs inputs one-to-one using a determinant.

The manuscript states that the main theorem and its corollary have been formalised in the Lean proof assistant and that Lean’s kernel has accepted them. The formalisation is in PSI’s repository. Jim Halverson, an adviser to PSI, checked the proof.

In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford University proved a consequence of the conjecture in the special case where the quantum algorithm reads its input in a fixed number of parallel rounds. PSI said the four had read the proof and were writing a shorter exposition of it for experts. In a message published on PSI’s page, they wrote: ‘This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups.’

The company published the manuscript itself. The sources do not mention peer review.