A proof of the Aaronson-Ambainis conjecture

An internally developed PSI research system, using a non-public Anthropic model, found a Lean-verified proof of the Aaronson-Ambainis conjecture, an open problem since 2008. The conjecture addresses whether quantum computers can gain exponential speedups on random inputs, rather than on structured problems such as factoring. A quantum algorithm that queries its input T times has an acceptance probability represented by a bounded polynomial of degree at most 2T. The conjecture says such polynomials must have a bit whose value substantially affects the output. This lets a classical computer inspect influential bits and estimate the quantum algorithm’s answer for nearly all inputs with only polynomially more queries. The result therefore rules out exponential quantum query savings for yes-or-no questions on random inputs unless the problem has rare structure.

The proof establishes that any nonconstant degree-d polynomial bounded between zero and one has a variable with influence at least c times its variance to the 5/2 power divided by d to the sixth, where c is about 0.0025. It follows a strategy by Shachar Lovett and Jiapeng Zhang, replacing an inequality they had left unresolved with a new one. The key argument pairs input settings using a determinant-based construction that strengthens a pairing supplied by David Reimer’s Butterfly Lemma. The system completed a proof on its third day, and Lean checked it; the result was then improved twice and checked again. PSI researcher David Turturean led the work, with an audit by Jim Halverson and comments on the formalization from Phiala Shanahan.