PSI says its system, running a non-public Anthropic model, proved the Aaronson-Ambainis conjecture and checked it in Lean

The announcement

On Nov. 6, Physical Superintelligence PBC (PSI) announced a proof of a conjecture in quantum complexity theory, saying that “the Aaronson-Ambainis conjecture is now a theorem.” The GitHub repository with the proof went public at 03:19 UTC that day, and the company’s X thread followed at 14:05 UTC. PSI says the proof was found by a research system developed internally and “running a non-public Anthropic model.”

According to PSI, multiple instances of that model were used in the run. The system had a complete proof during the third day of the run, and the Lean proof assistant accepted it. Neither the model’s name nor how PSI accessed it has been disclosed. No statement from Anthropic on the result could be found.

Physical Superintelligence@psipbc

Today Physical Superintelligence PBC is announcing a proof of the Aaronson-Ambainis conjecture, one of the central open problems in quantum complexity, with major implications for quantum computing speedup.

psi.inc/research/aaron…

Thread 👇

What the conjecture says

Query complexity counts how many times an algorithm accesses its input. A classical computer reads one bit of the input per query. A quantum query can spread across many positions in superposition. Large quantum speedups, such as Shor’s 1994 algorithm, rely on structure in the input, such as a repeating pattern. The conjecture concerns whether a quantum computer can answer yes-or-no questions with exponentially fewer queries when the input is completely random.

In 1998, Beals and colleagues showed that the probability of a T-query quantum algorithm saying “yes” is a polynomial of degree at most 2T. Aaronson and Ambainis conjectured that such a polynomial, with values between 0 and 1, always has an influential bit. If that holds, a classical algorithm can read the influential bits one by one. It can then predict the quantum algorithm’s output on most inputs with polynomially many queries. In other words, quantum speedups on unstructured problems are at most polynomial.

That does not make quantum computers useless. Exponential speedups remain possible on structured problems, and polynomial ones on unstructured problems. The Quantum Insider stresses that the result concerns query counts only and says nothing about total running time or commercial value.

The proof and the Lean check

According to the paper, a nonconstant polynomial of degree d with values between 0 and 1 has a bit with influence of at least c·v^(5/2)/d^6. Here v is the variance, and c = 8√15/(125π⁴), or about 0.0025. That bound is at least (v/d)^7. The conjecture asked for a bound of the form (v/d)^O(1); earlier general bounds shrank exponentially with the degree.

According to the paper’s appendix, the exponent was 22 in the first complete proof. Integration over “levels” brought it down to 11, and averaging over coordinates brought it to 7. All three versions were checked in Lean.

As a consequence, the acceptance probability of a T-query quantum algorithm can be approximated within error ε on a 1-δ fraction of inputs. A deterministic classical algorithm making at most (4T)^8·ε^-14·δ^-8 queries is enough. That makes three of Aaronson and Ambainis’ conditional results unconditional. One of them says that if P = P^#P, then BQP is contained in AvgP relative to a random oracle.

The formalization uses Lean 4.33.0 and Mathlib, with 84 modules, 648 theorems and 113 definitions and no added axioms. The four final theorems rely only on the propext, Classical.choice and Quot.sound axioms. The proof was replayed in two independent kernels, lean4lean and nanoda, and checked with Comparator. The repository also states what is out of scope. Readers must verify that the formal statement matches the conjecture, and the paper’s text was not machine-checked. The repository is licensed under Apache 2.0, while the paper’s copyright stays with its author.

The roles of AI and the team

According to the paper’s AI disclosure, the mathematical statements were generated by AI models. Model instances were used within the system to search existing ideas, propose new ones, combine and test them, and check other instances. A model wrote the first draft, and AI models also produced the Lean formalization. David Turturean reviewed and edited the draft and takes responsibility for its correctness.

Turturean, a member of technical staff at PSI, led the work and is the paper’s sole author. Advisor Jim Halverson checked the proof, and advisor Phiala Shanahan commented on the Lean formalization. PSI is a public benefit corporation. On Oct. 26, it announced that it had solved “five long-standing problems in quantum information theory.” Its website says it has raised more than $58 million in a round led by Breakthrough Energy Ventures; Matthew Pines is CEO.

History and reactions

According to Aaronson, the problem traces back to a question from Fortnow and Rogers around 1999, and Aaronson noticed the conjecture around 2008. The paper “The Need for Structure in Quantum Speedups” first appeared on arXiv on Nov. 5, 2009. It was presented at ICS 2011 and published in the journal Theory of Computing in 2014. In 2019, Nathan Keller and Ohad Klein claimed a proof. The preprint was withdrawn after Paata Ivanisvili found a flaw in Lemma 5.3.

In August 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan solved a special case. Their Aug. 19 paper shows that parallel quantum algorithms with t queries and d rounds can be simulated with t^O(d²) classical queries. The group has read PSI’s proof, sent comments and is writing a short exposition for experts. In remarks quoted by PSI, they call it “a huge result” that “resolves a decades-old conjecture.” They say the proof draws on and extends work in the analysis of boolean functions and probabilistic combinatorics.

The result has not been peer reviewed and is not on arXiv; the paper is available only as a PDF on GitHub. As of the morning of Nov. 8, Scott Aaronson had not commented on PSI’s proof.