AI-Assisted Proof Settles Aaronson–Ambainis Conjecture, Capping Quantum Speedups on Random Inputs

Quantum computers cannot solve every computational problem faster than conventional ones. The classic example is the factoring algorithm Peter Shor published in 1994. Shor's algorithm is dramatically faster than the best known classical algorithms because it exploits periodicity hidden in the underlying mathematical problem. In other words, the mathematical structure of a problem plays a decisive role in whether a quantum computer can show its strengths.

So can a quantum computer achieve an exponential speedup over classical computers even on random inputs, where no such structure is available? In 2008, Scott Aaronson and Andris Ambainis proposed a way to answer this open question in computational complexity theory through a statement in pure mathematics. Their work was posted to arXiv as a preprint (arXiv:0911.0996) and published in 2014 in Theory of Computing, Volume 10 (pp. 133–166). They showed that if the conjecture they posed is true, then for most uniformly random inputs, a quantum algorithm can be simulated classically with a polynomial number of queries.

On November 6, 2026, David Turturean of the research institute Physical Superintelligence (PSI) released a preprint claiming a proof of this "Aaronson–Ambainis conjecture." He also published formal verification code written in the proof assistant Lean 4. The result does not come from experiments on a physical quantum computer; it concerns a mathematical proof and its machine verification. The involvement of AI in the process, from discovering the proof to writing up the paper, has also drawn attention.

What Mathematical Structure Underlies Quantum Speedups?

The setting for this research is the "decision-tree query complexity model," which measures how many times an algorithm accesses its input data. Unlike ordinary running time, it ignores the number of internal operations the machine performs and counts only queries to the input as computational cost. A classical algorithm reads one bit of the input per query, whereas a quantum algorithm can make queries using a superposition of multiple bit positions. This difference is the starting point for thinking about quantum speedups.

In 1998, Robert Beals, Harry Buhrman, Richard Cleve, Michele Mosca, Ronald de Wolf and colleagues established an important result linking quantum query complexity to polynomial degree (arXiv:quant-ph/9802049). If a quantum algorithm makes $T$ queries, the probability that it accepts a given input can be expressed as a real polynomial in the input bits. The degree of this polynomial is at most $2T$, and because it represents an acceptance probability, its values on Boolean inputs always lie between 0 and 1. This made it possible to study the properties of quantum algorithms as a mathematical problem about polynomials.

Aaronson and Ambainis focused on how a classical algorithm could approximate such a bounded low-degree polynomial. If the value of the polynomial can be predicted with sufficient accuracy by examining only a few input bits, the acceptance probability of the quantum algorithm can also be estimated efficiently. They therefore conjectured that any bounded low-degree polynomial with at least a certain amount of variation over the whole input must have at least one variable with sufficiently large "influence." The new work resolves this long-standing question about quantum query complexity by proving that conjecture.

Bounded Low-Degree Polynomials Must Contain a High-Influence Variable

Let us lay out the main theorem that was proved. Consider the space ${0,1}^N$ of Boolean strings of length $N$, where each bit is 0 or 1. Let $p$ be a real polynomial in $N$ variables of degree at most $d$. Assume that $0\le p(X)\le 1$ for every Boolean input $X\in {0,1}^N$, and that for $X$ drawn from the uniform distribution, the variance of the polynomial satisfies $\mathrm{Var}[p]\ge ϵ>0$.

What matters here is the "influence" of each input bit on the value of the polynomial. If flipping a bit changes the polynomial's value substantially, that bit has strong influence. The influence ${\mathrm{Inf}}_i[p]$ used here is not a simple average of the change but the expected value of the squared change, defined as follows.

Here $X^i$ denotes the string $X$ with only its $i$-th bit flipped. Turturean's main theorem shows that for any polynomial satisfying the conditions above, at least one coordinate $i$ satisfies the following inequality.

The constant $c$ is given explicitly as follows.

The key point of this result is that the lower bound on influence does not depend on the total number of input variables $N$. No matter how many input bits there are, the existence of a variable with at least a certain amount of influence is guaranteed from the degree $d$ and the variance $ϵ$ alone. Moreover, the lower bound does not shrink exponentially with the degree $d$; it is given as an inverse polynomial. This property is the key to resolving the conjecture about quantum query complexity.

Previously, the known lower bounds on influence for general bounded real polynomials decreased exponentially as the degree $d$ grew. Early results were derived from a Fourier-analytic theorem shown in 2007 by Irit Dinur, Ehud Friedgut, Guy Kindler, Ryan O'Donnell and colleagues. But because the guaranteed influence shrinks rapidly as the degree grows, it was insufficient to guarantee the efficiency of the classical simulation that Aaronson and Ambainis needed.

For Boolean-valued functions, whose outputs are limited to 0 or 1, the corresponding property was already known from work on decision trees by Ryan O'Donnell, Michael Saks, Oded Schramm and Rocco A. Servedio (2005) and from work by Noam Nisan and Mario Szegedy (1994), among others. Progress was also made in various special cases by Ashley Montanaro (2012), Paata Ivanisvili (2026), Nikhil Bansal, Makrand Sinha and Ronald de Wolf (2022), and Francisco Escudero Gutiérrez (2023), among others. However, no one had been able to prove a lower bound on influence that is inversely polynomial in the degree for general bounded low-degree polynomials taking arbitrary real values between 0 and 1. This work is significant as the first to resolve this general case.

That said, it has not been proved that the exponents (the 5/2 power of the variance and the 6th power of the degree) or the coefficient $c$ are theoretically optimal. They were derived as explicit lower bounds sufficient to resolve the conjecture, and there is room for improvement. Also, this formulation represents input variables as $0,1$, whereas Boolean function analysis sometimes uses $-1,1$. Because the representation changes factors in the definition of influence, care is needed when directly comparing numbers from different formulations.

How Far Can Quantum Algorithms Be Simulated Classically?

With the conjecture that bounded low-degree polynomials contain a sufficiently influential variable now proved, the premise of the classical simulation theorem posed by Aaronson and Ambainis is satisfied. Theorem 3.3 in their original paper states that, if the influence conjecture holds, the acceptance probability of a quantum algorithm can be estimated efficiently by a classical algorithm. Specifically, for a quantum algorithm $Q$ making $T$ queries, there exists a deterministic classical algorithm that, for any chosen additive error $ϵ>0$ and exceptional fraction $\delta >0$, estimates the acceptance probability of $Q$ to within $ϵ$ on at least a $1-\delta$ fraction of inputs drawn from the uniform distribution.

The upper bound on the number of classical queries required is expressed as follows.

In other words, if the new proof is correct, this result, which previously depended on the conjecture, holds unconditionally. With the error $ϵ$ and the exceptional fraction $\delta$ fixed, the number of queries the classical algorithm needs stays within a polynomial of the quantum algorithm's query count $T$. Therefore, for uniformly random inputs, as far as approximating a quantum algorithm's acceptance probability in most cases is concerned, there is no exponential gap in the number of queries.

However, it would be a mistake to interpret this result as a refutation of quantum advantage. What the theorem guarantees is classical simulation under specific conditions, and its scope has important limits.

First, the guarantee concerns the average case, not the worst case. On the exceptional inputs, which make up at most a $\delta$ fraction of all inputs, the classical algorithm's estimation error may exceed $ϵ$. For example, if the solution to a problem is concentrated in a tiny part of the input space, this theorem alone does not imply that such special inputs can be handled efficiently. Moreover, the smaller the tolerated error $ϵ$ or exceptional fraction $\delta$, the more queries are needed.

Second, having the number of queries bounded by a polynomial is a separate matter from having actual running time bounded by a polynomial. The query complexity model evaluates only the number of accesses to input data and ignores the cost of the internal computation and memory operations needed between queries. Even if a classical algorithm can estimate an acceptance probability with polynomially many queries, the whole process need not finish in polynomial time. This theorem does not directly translate into faster practical quantum circuit simulators.

Third, what the classical algorithm approximates is a single number: the acceptance probability that the quantum algorithm ultimately outputs. It does not guarantee reproducing the entire quantum state vector inside the circuit, nor efficiently computing probability distributions for every possible measurement. This distinction is especially important when considering classically imitating quantum states composed of many qubits.

Fourth, this result does not rule out polynomial-order quantum speedups. For example, the square-root speedup of Grover's search algorithm is consistent with this theorem. Nor does the theorem alone negate quantum advantage for problems that exploit mathematical structure such as periodicity, as in Shor's algorithm. The same conclusion also cannot be applied directly to "promise problems," which concern only inputs satisfying specific conditions.

As related work, on August 24, 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford University announced an important partial result (arXiv:2608.19158). They proved that quantum algorithms with limited adaptivity, which query the input in a fixed number of parallel rounds, cannot achieve exponential speedups on random inputs. Turturean's result differs in that it resolves the conjecture for general adaptive quantum query algorithms, without such limits on the number of rounds.

How the Proof Works: Level Sets and the All-Pairs Inequality

Turturean's proof did not arise from entirely new ideas alone. An important foundation was the proof strategy using "fractional certificates" proposed by Shachar Lovett and Jiapeng Zhang in 2023 (LIPIcs.ITCS.2023.84). They presented a promising method for showing the existence of highly influential variables, but the combinatorial inequality needed to complete the method remained unproven. Turturean overcame this obstacle with a different inequality.

The basic idea of Lovett and Zhang is to divide the interval $[0,1]$, the range of the polynomial, by several thresholds and examine the sets of inputs whose values are at or above each threshold. These sets are called "level sets." For each level set, non-negative weights are assigned to the input bits, and the change in the function's value when multiple bits are flipped is bounded by the total of the corresponding weights. With this method, it may be possible to tie the behavior of the whole polynomial to the contributions of individual coordinates. But completing the proof required a particular combinatorial inequality, which remained an open problem.

Instead of directly proving the inequality that Lovett and Zhang conjectured, Turturean introduced a new "all-pairs inequality." Central to its proof is the analysis of the determinant of a matrix built from monomials and a bijection (one-to-one correspondence) constructed using its lowest-degree terms. By suitably matching points in the input space, this yields the required estimates.

This construction shares ideas with the "Butterfly Lemma" that David Reimer used in 1999 to resolve the van den Berg–Kesten conjecture. However, the matching from Reimer's method alone is too weak to yield the estimates needed here. Turturean incorporated a stricter condition that controls how much two matched inputs agree on particular coordinates. This constraint on coordinate agreement made it possible to prove the all-pairs inequality.

The proof proceeds step by step from this inequality. First, the all-pairs inequality is integrated over all level sets to derive an inequality about the third moment of the function. Next, from this third-moment estimate, it is shown that for at least one coordinate the mean absolute increment of the function's value is sufficiently large. Finally, averaging over coordinates connects the estimate of absolute increments to a lower bound on the influence ${\mathrm{Inf}}_i[p]$, which is defined via the mean square.

In this process, an upper bound of ${\pi }^2{d}^2$ on the weights of the fractional certificate is combined with an upper bound of $4d^2$ on pointwise sensitivity at each input point. Stacking these estimates produces the sixth power of the degree $d$ in the final influence bound. In this way, a polynomial-order lower bound was derived for general bounded real polynomials, for which only exponential dependence on degree had previously been obtained.

The results, and points to watch when interpreting them, are summarized below.

Issue	What was shown	Basis / verification status	Caveats
Main mathematical theorem	A bounded low-degree real polynomial has a variable with influence at least $(ϵ/d{)}^7$, independent of the total number of variables $N$.	Turturean's preprint and Lean 4 formal verification code	The exponents and coefficient of the lower bound have not been proved optimal.
Quantum query complexity	With fixed error $ϵ$ and exceptional fraction $\delta$, the acceptance probability of a quantum algorithm on most uniformly random inputs can be approximated with polynomially many classical queries.	Theorem 3.3 in Aaronson and Ambainis's 2014 paper and the new main theorem	It does not refute quantum advantage in general, and does not guarantee polynomial-time classical simulation.
Formal verification	Four main theorem declarations are reported to have passed verification by Lean 4 and multiple checkers.	Public GitHub repository. Uses Lean 4.33.0 and Mathlib v4.33.0	It does not automatically verify the semantic correspondence between the formalized statement and the original conjecture, nor the natural-language parts of the paper.
AI involvement	In PSI's own research environment, an undisclosed Anthropic model helped with discovering the proof, formalizing it, and drafting the paper.	PSI's announcement and the author's account of contributions	It does not show fully autonomous problem solving or reproducibility on other hard problems.

Formal Verification in Lean 4 and Its Limits

Another reason this work stands out is that formal verification code in Lean 4 was released alongside the paper presenting the proof. Lean is a proof assistant in which mathematical statements and proofs are written in a formal language and their logical correctness is checked by computer. With an ordinary paper, readers must work through each step of the proof to confirm its logic. With formal verification, a machine can check mechanically that the written proof follows the prescribed rules of logic.

The public repository contains four theorem declarations at the core of the proof. According to PSI, the proofs contain no placeholders such as sorry, which treats an unfinished part as if it were correct, and no improperly added custom axioms. Running #print axioms, which inspects axiom dependencies, reportedly showed that only three were used: propositional extensionality (propext), the axiom of choice (Classical.choice), and quotient soundness (Quot.sound). All are standard logical assumptions in Lean and the Mathlib mathematics library, and the explanation is that the proof does not depend on any special additional axioms.

The verification environment is specified as Lean 4.33.0 and Mathlib v4.33.0. According to PSI, the proofs were also rechecked with Lean's official tool leanchecker and verified with the independent type-checker implementations lean4lean and nanoda. Using multiple implementations reduces the risk that a faulty proof slips through because of a bug in a single verification system.

To illustrate why this matters, the public repository also includes a control experiment using deliberately false statements. With Lean's kernel verification disabled, code containing a false statement still succeeded under lake build, and no additional axioms were displayed. But when that code was rechecked with an independent checker, the false statement was rejected. The experiment shows that a successful project build alone cannot guarantee the correctness of formal verification, and that kernel checking of proofs is indispensable.

Still, formal verification does not automatically resolve every issue with a proof. Particularly important is whether the statement formalized in Lean (PrintedConjecture) expresses mathematically the same content as the original Aaronson–Ambainis conjecture. Lean can verify the correctness of a proof of a formalized statement, but it cannot automatically judge whether that statement matches the mathematical claim humans intended. Mathematicians must check whether the definitions have gaps or excess conditions and whether they faithfully express the original conjecture.

In addition, the paper's natural-language explanations, its survey of prior work, intuitive interpretations, and discussion of open problems are outside the scope of Lean's verification. Formal verification itself also presupposes that the kernel, the checker implementations, the underlying definitions, and the execution environment function correctly. Using independent checkers is an effective way to reduce reliance on this trusted base, but it does not eliminate all assumptions. The value of formal verification lies in clarifying what humans still need to check and in rigorously detecting logical errors in the formalized proof.

The public repository also contains a more advanced theorem, aaronson_ambainis_of_fbsDegreeBound, aimed at improving the constants. However, this theorem is a conditional result that assumes the conjectured boundary condition FbsDegreeBound introduced by Agarwal and Ben-David. Because that assumption itself is not formalized in the repository, the theorem should be distinguished from the unconditionally proved main theorem.

How Did AI Solve a Math Problem Open for 18 Years?

In this research, not only the mathematical conclusion but also how AI was involved in discovering the proof is an important point. According to PSI's published account, the research was led by David Turturean, a member of the institute's Technical Staff. Turturean designed a custom research harness, defined the scope of the problem to be solved, and then ran an AI system. The backend used an Anthropic AI model whose details have not been disclosed.

PSI reports that on the third day after the system started running, a complete outline of a proof resolving the Aaronson–Ambainis conjecture was obtained and passed Lean verification. Later, in the course of trying to apply it to related open problems, the lower bound on influence was improved twice, and the final formalization was completed. The first draft of the paper was also produced by prompting the model, but Turturean scrutinized the contents and takes responsibility for the mathematical validity. In addition, physicist and AI researcher Jim Halverson audited the proof, and Phiala Shanahan, a theoretical physicist at the Massachusetts Institute of Technology, advised on the Lean formalization.

Importantly, this result did not emerge from AI alone without human involvement. Human researchers set the problem and built the research environment, then combined AI-driven proof search with formal verification. While AI was also used to refine the proof and write the paper, the researchers were responsible for the final check of the content and for mathematical accountability. Also, the paper released is a preprint accompanied by a GitHub repository and has not completed journal peer review at this point.

PSI's announcement also includes favorable assessments from the Stanford researchers mentioned above, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan. The four read the proof closely and reportedly praised it as an important result resolving a long-standing conjecture, as well as for skillfully combining results from Boolean function analysis and probabilistic combinatorics. The announcement also notes that they are writing a concise explanatory article for experts. Such expert assessments are valuable evidence, but they are not themselves a formal peer-review process.

Caution is also needed in evaluating AI's capabilities. The record that a proof was obtained on the third day of operation and then improved twice is important for understanding the research process. But it alone cannot tell us quantitatively how likely the AI is to solve the same problem repeatedly, or how much it would raise the productivity of mathematical research. Systematic data have not been released on the detailed version and parameters of the model used, the structure of the prompts, comparisons with other models, or results of applying it to unrelated open problems.

It is therefore not accurate to describe this result as "AI fully autonomously solved a hard math problem." At the same time, it is significant that, within a human-designed research environment, combining AI reasoning with Lean formal verification led to a proof of an important mathematical problem that had gone unsolved for years. In particular, a mechanism that can formally check AI-generated proofs could become one of the key ways of bringing AI into mathematical research.

Challenges That Remain After the Limits of Quantum Computation Come Into Focus

The proof of the Aaronson–Ambainis conjecture shows that quantum speedups have clear limits depending on the nature of the problem. For uniformly random Boolean inputs, if a certain additive error and exceptional fraction are tolerated, the acceptance probability of a quantum algorithm can be approximated with polynomially many classical queries. This is an important theoretical constraint for thinking about the problems on which quantum algorithms can show an advantage. It does not, however, limit the time required for internal computation, nor quantum speedups on problems that exploit mathematical structure such as periodicity.

Going forward, the published proof and formal verification code are expected to undergo further scrutiny by mathematicians and theoretical computer scientists. Especially important will be checking the correspondence between the statement formalized in Lean and the original conjecture, and whether the result becomes established as mathematics through peer review. How far the degree dependence $d^{-6}$ in the influence lower bound can be improved also remains open. Whether the all-pairs inequality can be applied to other combinatorial conjectures related to the Lovett–Zhang proof strategy is another remaining research question.

This case is also an important test from the standpoint of AI-assisted mathematical research. Whether the combination of human problem-setting, AI proof search, and Lean formal verification is effective for other long-standing open problems, or whether this was the result of a particular problem fitting a particular research environment, will have to be judged through future cases. The result clarifies theoretical limits of quantum computation and is also an important step in considering how far AI can contribute to both discovery and verification in mathematical research.