PSI says a non-public Anthropic model proved the Aaronson-Ambainis conjecture, with a full Lean check

On November 6, Physical Superintelligence (PSI), a physics research lab structured as a public benefit corporation, announced a proof of the Aaronson-Ambainis conjecture, one of the best-known open problems in quantum query complexity. PSI says the proof was produced by an internal research system “running a non-public Anthropic model,” that the system had a complete proof during the third day of the run, and that the Lean 4 proof assistant accepted it. The formalization, the paper draft and the verification logs are public on GitHub.

If the proof holds, it settles a question theorists have worked on for well over a decade: whether quantum computers can be exponentially faster than classical ones on unstructured problems. The conjecture’s answer, now claimed as a theorem, is no. Exponential quantum speedups need structure in the input, which is roughly what Shor’s algorithm exploits and what random inputs lack.

What the conjecture says, and why it matters

Scott Aaronson and Andris Ambainis stated the conjecture in “The Need for Structure in Quantum Speedups”, first posted in November 2009 and published in Theory of Computing in 2014. In their words, “every bounded low-degree polynomial has a ‘highly influential’ variable.”

The precise version PSI proved: take a real polynomial p of degree at most d in N variables, with values between 0 and 1 on every input in {0,1}^N, and with variance at least ε over uniformly random inputs. Then some single variable i has influence at least (8√15/(125π^4)) · ε^(5/2) / d^6, and that is at least (ε/d)^7. The constant is about 0.0025. Influence here measures how much flipping bit i changes the polynomial’s value on average.

The link to quantum computing comes from a 1998 result by Beals, Buhrman, Cleve, Mosca and de Wolf: after T queries to its input, a quantum algorithm’s acceptance probability is a polynomial of degree at most 2T with values in [0,1]. That is exactly the kind of polynomial the conjecture is about. If every such polynomial has an influential variable, a classical algorithm can simulate the quantum one on most inputs by repeatedly reading the most influential bit until the remaining output barely varies. Aaronson and Ambainis showed this gives a poly(T)-query classical simulation on most inputs. One consequence they flagged in the original paper: under the conjecture, one essentially cannot hope to separate P from BQP relative to a random oracle.

Progress had been incremental. Earlier work by Dinur, Friedgut, Kindler and O’Donnell gave a bound that decays exponentially in the degree; O’Donnell, Saks, Schramm and Servedio handled the 0/1-valued case; and in August a team of Blanc, Docter, Strassle and Tan settled the simulation question for parallel quantum algorithms (a FOCS 2026 paper), showing a t-query, d-round algorithm can be simulated with t^O(d^2) classical queries on most inputs. The general case stayed open until this claim.

How the proof works

PSI’s proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang in their ITCS 2023 paper “Fractional Certificates for Bounded Functions”. Their approach reduced the conjecture to one inequality they could not prove and left as a conjecture. PSI’s system did not prove that inequality; it replaced it with a different one it could prove.

The repository’s overview breaks the argument into four parts:

1. An all-pairs inequality for Boolean functions, built from fractional certificates and a bijection between input settings produced by a determinant. PSI relates this to David Reimer’s “Butterfly Lemma,” which gives a weaker pairing; the new pairing also limits how often paired settings agree on each coordinate.
2. Integration over level sets of the bounded function, turning that into a third-moment inequality.
3. Averaging over coordinates to get the influence bound.
4. A row bound with sensitivity at every point, using Markov’s inequality, Chebyshev polynomials and LP duality, following a method from Agarwal and Ben-David.

After the first complete proof, PSI pointed the system at related problems, and it improved the result twice. Lean accepted the final version too.

What Lean actually checked

This is where the claim is stronger than most AI-math announcements, and also where its limits are clearest. According to the repository’s formalization guide and verification notes:

• Size. 84 files and 9,454 lines (6,446 of code), built on Lean 4.33.0 and the matching Mathlib release. The October 22 run counted 761 constants: 113 definitions and 648 theorems.
• No added axioms. #print axioms on the final theorems lists only Lean’s standard three (propext, Classical.choice, Quot.sound), and a static audit finds no sorry or native_decide in the library.
• Independent kernels. The proofs were replayed with Lean’s own checker and with lean4lean, a second kernel implementation, which reported 750,881 declarations checked. A Comparator run tested that the proved statement matches a reference statement that imports only Mathlib, so a reader can check the statement without trusting PSI’s definitions.
• One conditional theorem. Of four public theorems, three are unconditional, including the main one. The fourth, an improved constant, assumes a theorem from Agarwal and Ben-David that is not formalized.

The caveats are PSI’s own. The paper itself is not machine-checked, and whether the Lean statement faithfully captures the conjecture “is for a reader to confirm.” Every recorded run was made with the author’s tooling, rented machines or the repository’s own workflows, and “none has been repeated by another party.” The verification history comes from a private development commit.

That is also why this result is less fragile than OpenAI’s recent claimed falsification of the Exponential Time Hypothesis: the statement here is short, standard and written against Mathlib, so checking that the Lean theorem says the right thing is a small task for an expert.

Who did what, and what is still unknown

PSI credits David Turturean, a member of technical staff, with building the research system, scoping the problem, running it, and prompting the model to package the result into a first draft of the paper, which he reviewed and for which he takes responsibility. Advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the formalization. The repository states that the mathematical statements, the paper draft and the Lean code were produced by AI models.

PSI quotes the four authors of the parallel-algorithms paper, who it says are reading the full proof and writing a shorter exposition for experts: “This is a huge result.” We could not find a statement from them outside PSI’s page, and as of Saturday morning we found no public reaction from Aaronson or Ambainis.

Plenty is not disclosed. PSI does not name the Anthropic model, give the length of the run beyond “the third day,” or say how much compute it used, only that it ran “on our own infrastructure.” The company lists more than $58 million in funding led by Breakthrough Energy Ventures and a leadership team of Matthew Pines (CEO), Alex Wissner-Gross, Alex Klokus and Alessandro Morari. It published five results on open quantum problems in October.

What to watch

• Expert review. The Lean check makes an outright error unlikely, so the real test is whether specialists agree the formal statement is the conjecture as intended, and whether the promised short exposition appears.
• An arXiv posting. The paper currently lives only in the GitHub repository. A preprint posting would put it in front of the full community.
• Which model. A non-public Anthropic model doing frontier research for an outside lab is notable in itself. We found no comment from Anthropic on the result, and it would be worth knowing whether this is a research-access arrangement or an early look at an upcoming release.
• The pattern. Lean-verified results on named open problems now arrive from OpenAI, Anthropic-powered systems and smaller labs within weeks of each other. The bottleneck is shifting from finding proofs to having enough human experts to read them.