Physical Superintelligence published a Lean-checked proof of the Aaronson-Ambainis conjecture on 6 November. Found by an internal system running a non-public Anthropic model, the result would confirm that exponential quantum query speedups on typical yes-or-no inputs require rare structure. Shor’s algorithm is untouched.
On 6 November, Physical Superintelligence, a public benefit corporation that describes itself as an AI-native physics laboratory, posted what it says is a complete proof of the Aaronson-Ambainis conjecture. The conjecture, open since 2008, is a statement about low-degree polynomials. Scott Aaronson and Andris Ambainis showed that if it is true, a quantum computer cannot get an exponential saving in how many times it looks at its input, except on a small fraction of yes-or-no instances — unless those instances hide a rare pattern.
The company says an internal research system, running instances of a non-public Anthropic model on PSI’s own machines, produced a complete proof on the third day of a run. Lean, a proof assistant that checks every inference, accepted that proof and a later, tighter version. The accompanying paper and a Lean 4 formalization are public. Four Stanford theorists who had recently proved the same simulation claim for a restricted class of quantum algorithms, quoted by PSI, called it “a huge result.”
If the formal statement matches the conjecture — a step Lean does not perform by itself — a long-suspected rule of thumb in quantum algorithms would become a theorem in the query model: exponential speedups need structure. Factoring would remain as powerful as ever. What would be ruled out is an exponential query advantage on a typical, unstructured decision problem.
What “looks” have to do with quantum speedups
Most of the famous quantum algorithms are analyzed in the query model, also called the black-box or decision-tree model. The input is a long string of bits. A step that counts is a look at one of those bits. An ordinary computer reads a single position. A quantum computer can spread one look across many positions in superposition. Other computation is ignored; only the number of looks is scored.
In 1994, Peter Shor found a quantum algorithm that factors large integers far faster than any known classical method. The engine underneath is period-finding: the input is promised to repeat, and a quantum Fourier transform extracts how often. Simon’s algorithm and other exponential speedups rely on a similar kind of global regularity. Without that promise, the same techniques do not apply.
The opposite case is unstructured search. Grover’s algorithm finds a marked item among N possibilities with about √N looks, against about N classically — a quadratic saving, and one that is known to be optimal. For some total functions, such as parity, quantum algorithms offer no asymptotic saving at all.
The pattern suggested a law: superpolynomial quantum speedups exist, but only for structured problems. Formalizing that law took work. For total Boolean functions, Robert Beals, Harry Buhrman, Richard Cleve, Michele Mosca and Ronald de Wolf already showed in the late 1990s that classical and quantum query complexities are polynomially related. The interesting cases are partial functions, where a promise excludes most inputs, and average-case questions about random inputs.
Aaronson and Ambainis isolated a clean mathematical bottleneck in a paper first posted in 2009 and published in Theory of Computing in 2014 as “The Need for Structure in Quantum Speedups.”
The conjecture, in plain language
A T-look quantum algorithm’s chance of answering “yes” is not an arbitrary function of the input. Beals and his co-authors showed that it is a polynomial in the input bits, of degree at most 2T, and that its value always sits between 0 and 1. Estimating that probability, on most inputs, with only a polynomial number of classical looks would be enough to show that unstructured exponential speedups do not exist.
Aaronson and Ambainis reduced that task to a question about influence. Flip one bit of the input and see how much the polynomial’s value moves. The influence of that bit is the average of the squared change, taken over all inputs. The variance of the polynomial measures how much its value moves overall. Their conjecture says that if the polynomial is not almost constant, some bit has influence at least a fixed power of (variance / degree). In symbols, they asked for a bound of the form (ε/d)O(1).
That single influential bit is a handle. A classical algorithm that knows the polynomial can look at one highly influential unread bit after another. Each answer reduces the remaining variance. Once little variation is left, the algorithm outputs the average value as its estimate. The conjecture guarantees that a useful bit remains until that happens, and that the number of looks grows like a fixed power of T, not like an exponential.
PSI says it has proved a concrete version of that bound: some bit has influence at least (8√15 / (125π4)) · ε5/2 / d6, which is at least (ε/d)7. The leading constant is about 0.0025. The repository isolates the (ε/d)7 form in a Lean definition, PrintedConjecture, that imports only Mathlib, Lean’s standard mathematics library, so a reader can compare the formal statement with the printed conjecture without wading through the rest of the proof.
What the theorem would change — and what it would not
If that statement is the conjecture, several consequences follow from the 2014 paper rather than from any new physics.
On yes-or-no questions, a quantum computer could not save exponentially many looks unless the input had a rare pattern. Grover’s quadratic speedup would still sit inside the polynomial relationship. Shor’s algorithm would be untouched, because period-finding is the opposite of a random input: almost none of the possible strings satisfy the promise.
The result would also block the standard query-complexity route to separating BQP, the class of problems a quantum computer can solve efficiently, from classical polynomial time relative to a random oracle. Aaronson and Ambainis showed that, assuming their conjecture, if P equals P#P then with probability 1 a random oracle A would satisfy BQPA ⊆ AvgPA — quantum polynomial time would be simulable, on most instances, by a classical algorithm that is allowed to fail on a vanishing fraction of inputs. That is a statement about oracles and average-case complexity, not a proof that quantum computers are useless, and not a resolution of P versus BQP in the real world.
The theorem says nothing about how much time, memory or error correction a quantum machine needs. Query complexity counts looks at the input, not wall-clock time and not the cost of running Shor’s circuit. It also does not say that every interesting computational problem is unstructured. Hidden-subgroup problems, quantum simulation and other structured tasks remain the natural home of large quantum speedups.
In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford had already proved the simulation prediction for a restricted class of algorithms: every quantum algorithm that makes t looks in d parallel rounds can be simulated on most inputs with tO(d²) classical looks. That result, posted on 24 August as “Quantum Speedups Require Structure or Depth,” showed that unstructured superpolynomial speedups would need growing depth. PSI’s claim is stronger. It would cover algorithms that adapt arbitrarily, not only those with a bound on parallel rounds.
How PSI says the proof was found
David Turturean, a member of technical staff at PSI, led the work. According to the company’s announcement, he built the research system, chose the problem, ran the system on it, had the model package the results into a first draft of the paper, reviewed that draft and takes responsibility for the paper’s correctness. Jim Halverson, an advisor, audited the proof. Phiala Shanahan, also an advisor, commented on the Lean formalization.
PSI says the system had a complete proof on the third day and that Lean accepted it. The system then worked on related problems and improved the bound twice; Lean accepted the final version. The argument follows a plan of Shachar Lovett and Jiapeng Zhang, who in 2023 studied fractional certificates for bounded functions and left one inequality as a conjecture. PSI’s proof replaces that inequality with a new one, proved by pairing inputs through a determinant. The pairing strengthens David Reimer’s Butterfly Lemma, which already gave a weaker matching. The write-up also uses results of Avantika Agarwal and Shalev Ben-David; Raghav Kulkarni and Avishay Tal; and Yuval Filmus, Hamed Hatami, Nathan Keller and Noam Lifshitz.
Special cases of the conjecture were already known. It holds for polynomials that take only the values 0 and 1, by theorems of Ryan O’Donnell, Michael Saks, Oded Schramm and Rocco Servedio and of Noam Nisan and Mario Szegedy. Irit Dinur, Ehud Friedgut, Guy Kindler and O’Donnell proved a bound that decays exponentially in the degree rather than polynomially, which already implied an exponential — not polynomial — classical simulation. Ashley Montanaro, Paata Ivanisvili, Nikhil Bansal, Makrand Sinha and de Wolf, and Francisco Escudero Gutiérrez, among others, settled further restricted cases.
There has been a false dawn. In 2019, Nathan Keller and Ohad Klein posted a claimed proof. Aaronson wrote about it with enthusiasm, then added that the authors had retracted the preprint after Paata Ivanishvili found what then looked like a fatal flaw in a key lemma. That history is why a public machine-checked formalization matters more than another PDF.
What Lean actually certifies
Lean does not read English. It checks that each step in a formal development follows from the definitions and axioms it has been given. PSI’s repository documents an unusually careful verification chain for a first announcement: a static audit for the usual escape hatches (placeholders, extra axioms, hooks that bypass the kernel); an axiom report that lists only Lean’s standard foundational principles — propositional extensionality, classical choice and quotient soundness — behind the final theorems; kernel replay with leanchecker; a second replay with lean4lean, an independent type checker; and a comparator run that includes nanoda, a type checker written in Rust.
Those checks, as the repository itself warns, do not certify two things a reader still has to judge. First, that the Lean proposition named PrintedConjecture is the same statement Aaronson and Ambainis made in 2014. The authors wrote that definition in a file that imports only Mathlib, which is the right way to make the comparison possible, but the comparison is still a human job. Second, the paper is written for people and is not itself machine-checked. Several expository sections have no formal counterpart.
VibeCodAI has not independently replayed the Lean development. The verification claims above are those of the public repository and its documented workflows, not a separate audit.
Blanc, Docter, Strassle and Tan have been reading the proof, PSI says, have sent comments and are writing a shorter exposition for experts. Their note, as quoted by the company, calls the result huge, says it has important implications for which problems admit quantum speedups, and describes the argument as drawing together lines of work in the analysis of Boolean functions and probabilistic combinatorics “in a rather magical way.” That endorsement comes through PSI, not from an independent interview. Business Insider, which reported the announcement on 7 November, said Anthropic did not respond to a request for comment. As of 8 November, VibeCodAI did not find a public evaluation from Aaronson or Ambainis.
A theorem and a capability claim at the same time
PSI is not a university department posting a preprint. It is a company whose homepage argues that discovery can now run “at the speed of thousands of virtual minds,” and this proof is offered as evidence. The human credit is specified with unusual care — Turturean is responsible for correctness — and the Lean development is public, which is the opposite of a black-box demo. Both things can be true at once: the mathematics may hold, and the announcement is also a capability claim about an unnamed Anthropic model inside a proprietary research harness.
Frontier labs are already using their own models to speed up research. METR recently estimated that Anthropic’s internal systems are improving well-specified tasks about twice as fast as a year earlier. PSI’s announcement is the complement: an outside lab using a non-public Anthropic model to attack a named open problem, then posting the formalization.
That combination will invite a kind of attention the 2019 attempt did not. AI-assisted formal mathematics has been accumulating results for several years. A central conjecture in quantum complexity, with a public formalization and named expert readers, is a higher bar. It is also a higher-stakes place to be wrong. The responsible stance, until more experts have checked that the formal statement matches the conjecture and until specialists in the area have spoken, is to treat this as a serious, machine-checked candidate proof, not as a closed chapter of the textbook.
If the proof stands, the field will have a precise version of a lesson it has been teaching itself since Shor: the dramatic quantum speedups we know how to get are not a general-purpose discount on computation. They are discounts on problems that hide the right kind of pattern. The question that remains is the same one quantum algorithms research has been asking for three decades — which patterns still count, and which useful problems have them.