A proof of the Aaronson-Ambainis conjecture
David Turturean
cs.CC
Nov 6, 2026 · v1
quant-ph
TL;DR
The main theorem and its corollary for the Aaronson-Ambainis conjecture are formalized and kernel-checked in Lean, with a public repository.
Abstract
Aaronson and Ambainis conjectured that every bounded polynomial of low degree on the discrete cube has an influential variable. They showed that the conjecture implies that the acceptance probability of every quantum algorithm making $T$ queries can be approximated on most inputs by a classical algorithm making $\mathrm{poly}(T)$ queries. We prove their conjecture: every function $f\colon\{-1,1\}^n\to[-1,1]$ of degree at most $d\ge1$ has a variable of influence at least $c\,\operatorname{Var}(f)^{5/2}/d^{6}$, where $c>0$ is an absolute constant. In the original formulation, for polynomials of degree at most $d$ with values in $[0,1]$ on $\{0,1\}^n$ and variance at least $\varepsilon$, this gives a variable of influence at least $(\varepsilon/d)^{7}$. The proof is elementary, with steps inspired by works of others. Thus, as Aaronson and Ambainis anticipated, superpolynomial quantum speedups in the query model require structure, such as a promise on the inputs.
Problem
The Aaronson-Ambainis conjecture states that every bounded low-degree polynomial on the discrete cube has an influential variable. If true, the acceptance probability of any T-query quantum algorithm can be approximated on most inputs by a classical algorithm making poly(T) queries.
Approach
The elementary proof starts from a bijection theorem for permutations of the 1-set of a Boolean function, obtained from lowest-degree terms of a determinant. This yields a determinant inequality, then antipodal, all-pairs and two-sided inequalities. A row bound is proved via Chebyshev polynomials and LP duality, followed by integration over levels and averaging over coordinates. The statements were produced by AI models within a research harness, and the main results were formalized and checked in Lean.
Results
Every f: {-1,1}^n -> [-1,1] of degree at most d has a variable of influence at least c Var(f)^{5/2}/d^6. In the original {0,1} formulation this gives influence at least (ε/d)^7. Theorem 1.1 and Corollary 1.2 are kernel-checked in Lean.
