An AI lab reports a proof about the limits of quantum speedups
PSI reports a proof of the Aaronson–Ambainis conjecture. The important distinction is between looking up information and doing all the work needed to use it.
Reading tools for text size, copying, printing and your reading list
On November 6, research company Physical Superintelligence, or PSI, reported an AI-assisted proof of the Aaronson–Ambainis conjecture and made a formal proof project public. The claim addresses a longstanding question about when quantum computers can gain a dramatic advantage. Its practical meaning depends on exactly what the mathematics counts.
The relevant comparison counts queries: requests for information from an input. It excludes the other computational work performed between those requests. That distinction limits what the result can tell us about how quickly a machine would finish a real task.
What is inside the claim
The theorem PSI reports concerns polynomials, mathematical expressions formed by adding terms built from numbers and products of input variables. Here the Boolean inputs are strings of 0s and 1s, with every string equally likely. For expressions whose outputs stay between 0 and 1, PSI claims that if the outputs vary, at least one input bit must have a guaranteed influence when flipped. The size of that guarantee depends on the variation and the polynomial’s degree, which measures the highest combined power of variables in any term. At fixed variation and degree, the bound does not worsen as the input gets longer.
The quantum connection comes from Aaronson and Ambainis’s earlier work. Their reduction shows that proving this influence conjecture would let a deterministic classical algorithm approximate a quantum algorithm’s probability of answering yes on most uniformly random Boolean inputs. For fixed accuracy and a fixed permitted fraction of exceptions, the number of classical queries grows at most like a fixed power of the quantum query count.
Think of two researchers requesting documents from an archive. One asks for fewer documents but might spend much longer interpreting each one. Counting requests alone does not establish who finishes first. The analogy illustrates the accounting distinction, not how quantum hardware works.
The input distribution matters too. A guarantee covering most uniformly random strings need not cover every carefully structured input someone wishes to solve. Applying the result to a practical problem therefore requires checking the input model and the output being approximated.
A proof that can be inspected
PSI says its internal research system used a non-public Anthropic model. The repository credits David Turturean with developing the research harness and reviewing the paper, and says AI models produced the mathematical statements, first draft and Lean formalization. These are the team’s disclosures about the process; QubitWire has not reproduced the discovery run.
Lean is software for checking formal mathematical proofs. The repository supplies theorem statements, checking instructions and an audit of formal assumptions. Its scope boundary is explicit: the Lean development formalizes the polynomial influence result, while the paper’s discussion of quantum consequences has no formal counterpart in this project. The established reduction and the newly formalized theorem are separate parts of the argument.
Several questions remain distinct: whether a checker accepts the derivation, which assumptions it permits, and whether the formal statement matches the scientific claim. A successful software check provides evidence about particular steps in that chain.
The repository also separates its main formal library from a comparison test. Its audit explains that the placeholders in that test are not imported by the theorem library. Reading the authors’ audit does not reproduce it: QubitWire has inspected the public documentation but has not independently rebuilt or replayed the proof.
Public scrutiny has begun
A contributor using the GitHub name heathsanchez has proposed a separately stated interpretation of the original conjecture and a formal implication from PSI’s theorem to that statement. The unmerged pull request reports a successful build, checks of the assumptions and a replay of the 84 project modules. Its linked GitHub Actions run shows success, and the published workflow pins the proposed version and invokes those checks. QubitWire inspected those pages but has not reproduced the run.
The contributor explicitly limits the result: it does not verify the quantum-query reduction or settle the intended meaning of the informal conjecture. The visible workflow replays the project modules; it does not invoke the repository’s separate procedure for replaying all dependencies from an empty environment. These checks should be reported at their stated scope.
PSI separately says Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan have read the proof, sent comments and are preparing a shorter exposition. That account and their assessment appear in PSI’s announcement, rather than in a separately published review inspected for this article.
What to watch next
Broader expert assessment and clearly documented reproductions would help establish how the formal theorem relates to the original problem. Readers can already inspect the public contribution while recognizing its limits.
For AI research, the release provides a mathematical artifact and a disclosed account of how it was produced. For quantum computing, its significance rests on the theorem’s precise scope. It supplies no hardware benchmark or general fast classical replacement for a quantum computer.
The practical reading remains straightforward: fewer requests for information do not automatically mean less computing time. Both the promise and the limits of this result depend on keeping those quantities separate.