What did the AI system actually prove?
On 6 November 2026, the research lab Physical Superintelligence published a paper and a Lean formalization. PSI says an internal system found a complete proof of the Aaronson-Ambainis conjecture. The run used instances of a non-public Anthropic model on PSI's own infrastructure.
According to PSI, the first complete proof appeared during the third day of the run. Lean, a proof assistant that checks every logical step, accepted it. PSI then asked the system to work on related open problems. The system improved its own bound twice, and Lean accepted both revisions.
The final paper is credited to David Turturean, who built the research harness. The disclosure is unusually direct. It says the mathematical statements, the first draft and the Lean formalization were produced by AI models. Turturean says he reviewed and edited the paper and is responsible for its correctness.
The paper also describes the division of labour inside the run. Multiple instances of the model searched the literature, proposed ideas, combined approaches and tested arguments. Some instances coordinated the work of others. A human chose the problem and operated the system.
The theorem itself is about polynomials, not quantum circuits. Take a real polynomial on the Boolean cube whose values stay between minus one and one. Suppose its degree is at most d. If the polynomial varies enough across inputs, then at least one coordinate must have a large influence.
Influence measures how much the polynomial changes, on average, when one input bit is flipped. The new proof guarantees an influence of at least c times Var(f) raised to 5/2, divided by d to the sixth power. The paper gives an explicit constant of about 7.95 times ten to the minus five.
In the notation used by Aaronson and Ambainis, the same result reads as follows. A bounded polynomial of degree d with variance at least epsilon has a variable of influence at least (epsilon/d)^7. That exponent of 7 is the concrete answer to a question the original authors left open.
The formalization covers the main theorem and its corollary. It does not formalize every remark in the paper. The repository lists which printed statements have no Lean counterpart, including the discussion of consequences and open questions.
Why did the Aaronson-Ambainis conjecture matter?
The conjecture sits at the centre of quantum query complexity. In that model, a computer is charged for each request it makes to an input. A classical query reads one bit. A quantum query can act on many positions in superposition.
Peter Shor's 1994 factoring algorithm shows the power of structure. Its input hides a repeating pattern, and the quantum computer finds the period. Simon's problem relies on a similar promise. Most inputs have no such pattern, which raises a harder question.
Can a quantum algorithm be exponentially faster on random inputs? Scott Aaronson and Andris Ambainis turned that question into a statement about polynomials. They also showed that their conjecture implies a broad simulation result. A classical machine could mimic a quantum algorithm on most inputs with only polynomially more queries.
The conjecture dates to a 2008 lecture by Aaronson at a Banff workshop. It appeared as Conjecture 1.7 in their paper The Need for Structure in Quantum Speedups, published in Theory of Computing in 2014. The paper calls the underlying statement folklore.
The link to quantum algorithms comes from the polynomial method. Beals, Buhrman, Cleve, Mosca and de Wolf showed that a T-query quantum algorithm's acceptance probability is a polynomial of degree at most 2T. The polynomial is bounded between zero and one.
If every such polynomial has an influential variable, a classical algorithm can simulate the quantum one. It reads the most influential bit, fixes it, and repeats. The new paper gives an explicit cost of at most (4T)^8 epsilon^-14 delta^-8 queries for this procedure.
Aaronson and Ambainis framed the same idea as a folklore conjecture about algorithms. It says a T-query quantum algorithm can be approximated on all but a delta fraction of inputs by a deterministic classical algorithm. That classical algorithm may use a number of queries polynomial in T, 1/epsilon and 1/delta.
The two statements are equivalent in their framework. Proving the polynomial version therefore proves the algorithmic one. The paper notes that the earlier polynomial bounds grew exponentially with degree, which was not enough to imply a polynomial simulation.
That is a polynomial in T, but a steep one. For a fixed error tolerance and a fixed fraction of excluded inputs, the growth is no worse than polynomial. The result therefore supports a broad intuition. Exponential quantum speedups should require a promise or other structure in the input.
The consequence is narrower than it may sound. The theorem limits input reads, not total running time. It also allows polynomial quantum advantages on unstructured problems, and it leaves structured problems untouched.
How was the proof checked?
PSI published the paper with Lean code, build scripts and verification records. The Lean development targets version 4.33.0 with Mathlib v4.33.0. The repository is public under the Apache 2.0 licence, and the paper's LaTeX source and PDF sit beside the formalization.
The checks go beyond a successful build. The authors say the sources contain no sorry, no axiom, no unsafe declaration and no way around the kernel. For each of the four final theorems, the axiom report lists exactly propext, Classical.choice and Quot.sound. Those are standard Lean principles used through Mathlib.
Two independent kernel implementations replay the proofs. One is Lean's own leanchecker, which checks declarations outside the elaborator. The other is lean4lean, a separate type checker. The project also includes a control case. A false statement with the kernel disabled passes a normal build, and both checkers reject it.
A separate tool called Comparator compares the final theorems against a challenge file. It replays the proofs with nanoda, a type checker written in Rust, and with a Lean kernel. PSI reports that a sandboxed run hosted by GitHub accepted all four theorems.
Human review matters here too. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford had proved a restricted version in August 2026. They read the full proof, sent comments, and are writing a shorter exposition for experts. The paper thanks them and says Aaronson referred PSI to the group.
In a statement quoted by PSI, the Stanford researchers called the work a huge result. They said it resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups. That is expert opinion, not a formal peer review, but it is a meaningful signal.
The verification has a clear boundary. Lean checks that the proof follows from the stated definitions. It does not check that the formal statement matches the conjecture as printed in 2014. That comparison is left to human readers, and the repository publishes both statements side by side. It also pins the toolchain and records source digests, so others can replay the checks.
What are the limits of the result?
The theorem lives in the query model. It counts how often an algorithm reads its input, not how much work it does between reads. A classical simulator might use few queries yet perform an enormous amount of computation. The paper is explicit that this does not settle total running time.
The guarantee also holds for most inputs, not all of them. The classical algorithm may fail on a small fraction delta, which the user chooses. The cost then depends on delta, and on the accuracy epsilon, through steep exponents.
The explicit bound is generous. The paper's own analysis allows a substantial number of queries when high accuracy is required. Avoiding exponential growth does not make the simulation practical. This is a statement about asymptotics and structural limits, not an engineering recipe.
The constant is also not optimized. The paper notes that its influence bound can be multiplied by four using a stronger result from Agarwal and Ben-David. A further factor of two is available from work by Filmus, Hatami, Keller and Lifshitz. These are refinements, not changes to the exponent.
The proof also leaves mathematical work open. The strongest possible influence bound is not established. The central matching step is shown to exist through an algebraic argument, not through a direct construction. A more explicit method could make the argument easier to audit and extend.
One formalized theorem depends on a hypothesis from separate work by Agarwal and Ben-David. That hypothesis is not formalized in the repository. The main theorem and the printed conjecture do not rely on it, but readers should note the distinction.
The AI claim has limits of its own. This is a single case study, on a problem chosen and scoped by a human. The model is not public, and PSI has not released its weights, size or version. Nothing here shows the system would repeat the result on an unrelated open problem.
Caution is warranted because this field has seen premature claims. The paper notes that an elegant 2019 attempt by Nathan Keller and Ohad Klein, titled Quantum speedups need structure, was later withdrawn. Formal verification and expert review raise the bar, but they do not remove the need for scrutiny.
Who is affected by the proof?
Quantum algorithm researchers get a sharper map of where to search. Exponential advantages should come from problems with promises, symmetries or other exploitable structure. That was already the working intuition. It is now a theorem in the query model, assuming the formal statement is accepted.
Complexity theorists gain a tool with consequences beyond simulation. Aaronson and Ambainis showed that their conjecture implies bounds on approximate decision trees. It also bears on whether BQP and AvgP can be separated relative to a random oracle. The new paper notes that such a separation would require proving P is not equal to P#P.
The AI-for-mathematics community gets a prominent test case for formal verification. Lean did not discover the proof. It acted as a filter that a candidate proof had to pass. The disclosure keeps that division explicit: models generated the material, and a named human reviewed it.
AI labs get an evaluation data point they cannot fully inspect. A non-public Anthropic model reportedly produced research-level mathematics inside a human-built harness. The result is notable, but the missing model details limit what anyone outside PSI can conclude about capability or reliability.
Students and teachers may notice a textbook change. Ryan O'Donnell's Analysis of Boolean Functions presents the conjecture in the notes to Chapter 8. It observes that, if true, the conjecture would have significant consequences for the limitations of efficient quantum computation. That conditional sentence now has a proved premise.
What should readers watch next?
The first thing to watch is independent mathematical review. The Stanford group is preparing a shorter exposition for experts. That document will make the argument easier to check and will show whether the proof's new ingredients hold up under expert reading.
The second is peer review and publication. The paper is a preprint with a formalization, not a journal article. Formal verification reduces the risk of a hidden gap. It does not certify novelty, significance or the fidelity of the formal statement to the original conjecture.
The third is follow-up work. The paper points to sharper influence bounds and a direct construction for its matching step. Other researchers have already been studying distributional variants of the conjecture. A 2026 preprint by Girish, Mittal, Nehoran and Raz examines that direction, and the new theorem may change those questions.
The Stanford paper is heading to FOCS 2026, a major theory conference. It shows that t-query quantum algorithms with d rounds can be simulated by classical algorithms using t to the order d squared queries. The full-conjecture proof goes further, but the two results will be read together.
The fourth is disclosure. PSI has described its harness but not the Anthropic model behind it. Replication would require either more detail or a comparable public model. Without that, the result remains a documented one-off rather than a general capability claim.
The fifth is the practical meaning for quantum computing. The theorem does not reduce the value of quantum algorithms for chemistry, optimisation or cryptography. It clarifies why those algorithms need structure. It also suggests that claims of exponential speedup on unstructured data deserve close scrutiny.
For now, the safe summary is conditional and precise. PSI reports that an AI system found the proof, and the Lean development is public. Experts are reading the argument. The conjecture, open since 2008, now has a claimed proof with machine-checked core theorems and a clear list of what remains unchecked.