A proof of the Aaronson–Ambainis conjecture shows where a particular quantum advantage runs out. The public manuscript and Lean files also reveal what others can verify when a mathematical discovery comes from a private AI system
An artificial intelligence system can make a persuasive mathematical claim long before anyone knows whether it has proved it. The harder achievement is to produce a chain of reasoning that other people can inspect, in a form precise enough for a proof checker to verify. On 6 November 2026, Physical Superintelligence, or PSI, announced a proof of the Aaronson–Ambainis conjecture, a longstanding problem about when quantum computation can offer a large advantage. The company attributes the discovery to an internal research system using a non-public Anthropic model. It released both a manuscript and a formal proof (PSI research announcement.)
The result has two kinds of significance. For quantum computing, it gives a mathematical explanation of a limit on what certain algorithms can gain from quantum access to their inputs. For AI research, it illustrates how an artefact produced with a private system can become open to scrutiny. The evidence for the first claim is in the proof. The evidence for how that proof was found comes chiefly from PSI’s account of its experiment. The distinction matters whenever a company presents a result as evidence of both a discovery and the capabilities of the system that produced it.
On 8 November, Scott Aaronson, one of the two researchers who posed the conjecture, wrote that he believed the proof was correct. He pointed to the Lean certificate and to experts who had studied the proof, and linked to an exposition by Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan. Aaronson was also explicit that he had yet to understand the proof himself. His response is a public expert assessment with a stated basis. The manuscript remains a preprint, and this assessment is distinct from a formal journal review.
What kind of quantum advantage is at issue?
Imagine being given access to a long sequence of bits through an interface that answers queries about it. The query model counts how many times an algorithm uses that interface. A classical query can inspect a position. A quantum query can act on a superposition of positions, allowing a calculation to exploit interference when it combines information. The metric deliberately separates access to the input from the work between queries. An advantage in that metric can be theoretically revealing even if it says little about elapsed time on a particular computer. A simulation that uses relatively few classical queries can still be expensive to carry out.
Aaronson and Andris Ambainis asked what could be said about such advantages when the input lacks a special promise and the algorithm’s output is a decision. Their original paper showed that if a conjecture about bounded polynomials held, a classical algorithm could approximate a quantum algorithm’s output probability on most uniformly distributed Boolean inputs with a number of queries polynomial in the quantum query count, at fixed approximation and failure tolerances. The result is about typical inputs under those conditions. It leaves room for advantages that exploit special structure and for questions that ask for a different kind of output
A useful comparison is between an algorithm supplied with a promise about the data and an algorithm asked to work across typical strings. A promised pattern can make certain relationships among input positions meaningful, even when any particular position tells the reader little. A result about random inputs cannot be applied indiscriminately to such a task. Aaronson highlights Shor’s factoring algorithm as an example whose relevant subroutine exploits periodicity. The new proof sharpens a boundary in computational complexity. Its practical significance for an application depends on what structure that application supplies and what quantity an algorithm is meant to compute.
Why the problem becomes one about influence
The link from computation to algebra comes from representing the probability of a yes answer as a polynomial in the input bits. A quantum algorithm making a limited number of queries gives rise to a polynomial of limited degree. Degree describes the maximum number of variables multiplied together in any one term after simplifying the expression on Boolean inputs. The expression can nevertheless involve a very large number of distinct variables. The conjecture asks whether a bounded polynomial with substantial variation and limited degree must have at least one variable that matters by a quantitatively meaningful amount.
For an illustrative example, picture a number calculated from many binary features. If flipping one particular feature often changes the number considerably, it is worth learning that feature before trying to predict the value. The technical notion of influence makes this idea precise by averaging the squared change when a bit is flipped. The difficult part is showing that a sufficiently influential feature exists even when the dependence is spread across many variables. The new preprint bounds the influence of some variable from below in terms of the degree and variance, with no direct dependence on the total number of variables.
That independence from the total number of variables is what makes the bound relevant to the query question. A classical procedure can inspect a variable that reduces uncertainty, then repeat the reasoning with that variable fixed. If the remaining variation is already small, it can approximate the value without inspecting every position. This explains the role of the bound at a high level. The actual argument needs to control how many such steps are required and how often its estimate succeeds. In August 2026, Blanc and colleagues had proved a related simulation result for algorithms with a limited number of parallel query rounds, a special case that helps put the later result in context.
Finding the proof and checking the proof
According to PSI, its system reached a complete proof on the third day of the run and subsequently improved the result. The company identifies Turturean as the researcher who developed the system, scoped the problem and reviewed the manuscript, and says Jim Halverson audited the proof. The mathematical argument builds on existing work, including a strategy due to Shachar Lovett and Jiapeng Zhang. Those contributions clarify what was involved in turning a research run into a result that can be read. The record supports a claim about this particular combination of model, research software, prior mathematics and human review.
Lean performs a different job from the language model. A formal proof states the definitions, assumptions and conclusion in a language the proof assistant can process. The checker then verifies that the conclusion follows from accepted steps. A successful check provides evidence for the formal statement under the relevant assumptions. People still have to establish that the statement expresses the intended mathematical problem and explain why the argument works. Here, a reader can compare the original conjecture with the manuscript and the formal files. The public repository makes that comparison possible without access to the private discovery system.
There is a second distinction between rerunning the checker and rerunning the discovery. The former starts with the completed argument and asks whether it passes a specified verification procedure. The latter would need the model, the research environment, the instructions and an account of what choices people made along the way. The company describes the model as non-public. The disclosed materials therefore provide much more direct access to the proof than to the method that found it. Those forms of reproducibility answer different questions, one about the validity of an artefact and the other about the reliability of a process.
How to judge the next discovery
A single research success gives little basis for estimating how often a system will solve other difficult problems. A stronger evaluation of the discovery process would disclose how problems were chosen, the number of attempts, the time and computation allowed, and how candidate proofs were screened. It would also describe the interventions that mattered, including whether a researcher supplied a promising lemma or changed the scope after a failed attempt. Such information could help separate a useful contribution to a team from a capability that can be expected across a broader range of problems. The November announcement reports a result rather than a comparison under those conditions.
Research teams may still learn from the division of labour on display. A model can explore candidate arguments while a formal environment makes some errors visible and allows valid pieces to be retained. Specialists can assess whether the formulation matches the intended problem, connect the result with previous work and communicate the proof to others. This arrangement has particular appeal when a proposed result can be expressed precisely enough to check. In other kinds of science, the corresponding evidence may require a new measurement or experiment. A formal certificate for a mathematical claim cannot stand in for those empirical tests.
The most durable outcome of the announcement is the argument other researchers can study and use. Its origin invites further questions about how to build research systems, how to credit the people and ideas behind their outputs and how to measure the costs of discovery. Those questions can be pursued because the mathematical claim travels separately from the system that produced it. A reader can examine the exact boundary the theorem draws, follow the proof and ask where the technique might apply next, even while much about the private research run remains unknown.
Image credit: Dilution Refrigerator, photograph by Pavlos Apostolidis, published by UCL Mathematical & Physical Sciences, CC BY 2.0. Illustrative image of quantum research equipment. The source file is unedited. WordPress may resize or crop display versions.
