PSI AI System Proves Aaronson-Ambainis Conjecture, Ending 18-Year Quantum Complexity Open Problem

The Aaronson-Ambainis conjecture is a quantum complexity conjecture posed in 2008 by Scott Aaronson and Andris Ambainis, asserting that every bounded low-degree boolean function has a variable that significantly influences its output.

Physical Superintelligence (PSI) said on Nov. 6, 2026, that an internal research system running on PSI infrastructure produced a complete proof of the Aaronson-Ambainis conjecture, a quantum complexity problem that had resisted proof since Scott Aaronson and Andris Ambainis posed it in 2008. The system, which used instances of a non-public Anthropic model, generated its first Lean-verified proof on the third day of the run and then improved the bound twice more. Four Stanford researchers — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — have reviewed the proof and are preparing a shorter exposition for experts.

The conjecture concerns the analysis of boolean functions, the mathematical study of functions whose inputs are strings of bits. It states, informally, that every polynomial of bounded degree on the discrete cube must have at least one variable that materially influences the function's output. The question carries weight in quantum complexity because it governs which computational problems can exhibit quantum speedups: if low-degree functions always have influential variables, certain classes of quantum algorithms cannot outperform classical ones on those functions.

Aaronson and Ambainis formulated the conjecture in 2008 as a barrier result, aiming to characterize when quantum algorithms fail to provide an exponential advantage. The conjecture's central quantity is the influence of a variable — how much a function's value changes, on average, when that variable is flipped. The 18-year gap between the conjecture's statement and a proof made it one of the most visible open problems in the analysis of boolean functions and quantum complexity theory.

What is the Aaronson-Ambainis conjecture and why does it matter?

The conjecture is a statement about bounded polynomials on the discrete cube {0,1}^n. A function f on the cube has degree at most d if it can be expressed as a real polynomial of total degree at most d. The influence of variable i, written Inf_i(f), measures how often flipping that variable changes f's output. The conjecture asserts that for any such f with variance Var(f), there exists a variable whose influence is at least a constant times Var(f)^(5/2)/d^6.

That bound has a direct algorithmic reading. In the original formulation, the influence lower bound is (ε/d)^7 for functions whose variance is at least ε. A proof of the conjecture rules out a broad family of potential quantum speedups, because it implies that a low-degree boolean function cannot hide its sensitive variables — a property that quantum algorithms could otherwise exploit. Researchers in quantum computing and complexity theory have cited the conjecture as a key stepping stone for understanding the limits of quantum advantage.

Importantly, the conjecture does not say every boolean function has an influential variable; high-degree functions such as parity can have all variables equal. The restriction to bounded polynomials of degree at most d is what makes the statement nontrivial and what connects it to quantum algorithms that operate on low-degree encodings of inputs.

The influence formulation also connects to learning theory and social choice, where influence bounds control how much a single coordinate can affect a function. A theorem of this form limits the extent to which any one input bit can dominate a function's behavior, a property relevant to questions about noise stability, dictatorship testing and the structure of voting rules.

How did the PSI research system produce and verify the proof?

PSI described the proof as the work of a research system the company developed internally, rather than of a single model invocation. The system scoped the problem, generated candidate mathematical statements, and checked each step against the Lean 4 proof assistant. On the third day of the run, it had a complete proof that Lean accepted. PSI said the system then improved the mathematical bound twice more, with each successive version also passing Lean's verification.

1. David Turturean of PSI scoped the problem and developed the research harness that drove the proof search.
2. Instances of a non-public Anthropic model generated candidate arguments within the harness.
3. Lean 4 verified each candidate step, rejecting invalid reasoning and accepting the complete proof on day three.
4. The system improved the bound twice more, producing stronger theorems that Lean also accepted.
5. Turturean prompted the initial draft of the paper, reviewed the output, and took responsibility for correctness.
6. Stanford researchers reviewed the full proof, sent comments, and began writing a shorter expert exposition.

PSI published the result in a research note and made the formalization public in a GitHub repository. The repository contains a paper and a Lean 4 formalization of the proof, with four theorems proved with no placeholder and no added axiom. PSI stated that the proof, the paper and the formalization were produced by AI models; the human role was limited to building the harness, scoping the problem, prompting the draft, and reviewing the final output.

PSI said instances of a non-public Anthropic model were used in the run, but the company's announcement focused on the research system rather than on the model's architecture or training. Because the model is non-public, the exact configuration used in the run is not available to outside researchers.

What does the proved theorem actually say?

The proved theorem gives an explicit constant. For every bounded real polynomial p of degree at most d on the discrete cube, some variable i satisfies Inf_i[p] ≥ (8√15/(125π^4)) ε^(5/2)/d^6, where ε is the variance of p. The constant 8√15/(125π^4) is approximately 0.0025. PSI notes that this is equivalent to the lower bound (ε/d)^7 in the original formulation of the conjecture.

The proved theorem at a glance

Component	Statement
Setting	Bounded real polynomial p of degree at most d on the discrete cube {0,1}^n
Guarantee	There exists a variable i with influence Inf_i[p] meeting the bound
Influence bound	Inf_i[p] ≥ (8√15/(125π^4)) ε^(5/2)/d^6
Constant	8√15/(125π^4) ≈ 0.0025
Original formulation	Equivalent to Inf_i[p] ≥ (ε/d)^7

The explicit constant matters for downstream use. An asymptotic proof might have shown only that some constant exists; the explicit value lets other researchers plug the bound into their own calculations without redoing the proof. The proof's structure, according to PSI, draws on and extends several lines of work in the analysis of boolean functions and probabilistic combinatorics.

The discrete cube setting means the result applies to functions on bit strings, the natural domain for boolean functions in circuit complexity and learning theory. The bound's dependence on variance, rather than on the function's size, makes it scale-invariant: multiplying f by a constant multiplies both sides of the inequality, so the ratio between influence and variance is unchanged.

Who reviewed the result and what did they say?

The Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan had settled a special case of the conjecture in August 2026, months before PSI's announcement. That prior result gave the group standing to assess the full proof. According to PSI, the four researchers have read the proof of the full conjecture, sent comments, and are writing a shorter exposition of it for experts.

This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups. The proof draws on and extends several lines of work in the analysis of boolean functions and probabilistic combinatorics. Everything is brought together in a rather magical way.Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Stanford researchers

The quote's emphasis on the proof's breadth reflects the structure of the result. The conjecture sits at the intersection of boolean function analysis, probabilistic combinatorics and quantum complexity; a proof that resolves it must connect techniques from all three fields. The Stanford group's decision to prepare an expert exposition is a signal that they regard the result as both correct and mathematically interesting enough to make accessible to the broader community.

What are the market and stakeholder implications?

The result is a milestone for AI-driven mathematical research, but it also carries implications for the companies and research groups building AI systems for science. PSI used a non-public Anthropic model, underscoring the competitive value of frontier models that are not broadly released. The announcement suggests that the combination of a capable model, a formal verification tool, and a carefully designed research harness can produce publishable mathematics in days rather than years.

For enterprises, the episode illustrates a workflow pattern: an AI system proposes, a proof assistant disposes. Lean 4's role as a referee removed much of the risk of hallucinated arguments that has historically limited AI-generated mathematics. The fact that the system improved its own bound twice — rather than stopping at the first valid proof — points to a search process that can iterate beyond a single correct answer.

For academic mathematics, the episode raises questions about the pace of research and the division of labor between humans and machines. The Stanford reviewers contributed the traditional human functions: verification of the argument, commentary, and exposition for experts. PSI's Turturean took responsibility for correctness, a governance choice that assigns accountability to a named human even when the mathematical statements and Lean code were produced by models.

The episode may also accelerate interest in formal verification infrastructure. Proof assistants such as Lean are becoming standard tools in AI research pipelines because they turn model outputs into checkable objects. Researchers who would not trust an LLM's prose may accept a Lean certificate, which is mechanically verifiable.

What happens next?

The near-term next step is the shorter exposition from the Stanford group, which will make the proof easier for researchers to check by hand. PSI's repository already allows independent verification of the formalization, since Lean accepts only proofs it can check mechanically. The company said the research harness used for the project can be repurposed for other open problems.

Longer-term, the result is likely to feed into research on the limits of quantum speedups and into the growing literature on machine-verified mathematics. The conjecture's resolution does not by itself prove that quantum computers cannot outperform classical ones, but it removes one of the theoretical structures that might have enabled certain speedups. Researchers will now need to incorporate the bound into subsequent work on boolean function analysis and quantum algorithms.

PSI's announcement describes the Stanford review as the external validation step so far; it does not describe submission to a refereed journal. The public Lean formalization, however, gives any researcher the ability to check the proof mechanically, independent of the Stanford group's reading.